Refactor documentation of properties

[williamdemeo]

Description

This closes issue #965.

Copilot Generated Description

This pull request removes the outdated Properties.md summary file and replaces it with individual markdown files for each formally stated or proved property in the ledger specification. Each property now has its own dedicated documentation page, with improved cross-referencing and explicit section anchors for easier navigation. The changes also update the navigation and link references to reflect this new structure.

Documentation Restructuring:

• Removed the old Properties.md summary file from both the documentation sources and navigation, eliminating the previous aggregation of ledger properties. [1] [2] [3]
• Added standalone markdown documentation files for each property, such as Certs/Properties/PoV.lagda.md, Certs/Properties/PoVLemmas.lagda.md, Certs/Properties/VoteDelegsVDeleg.lagda.md, and similar files for chain and epoch properties. Each file contains a dedicated section with an explicit anchor for the property or theorem. [1] [2] [3] [4] [5] [6] [7] [8]

Content Improvements:

• Updated the property documentation to clarify informal statements, add explicit theorem/claim anchors, and improve the presentation of Agda code and proofs (including toggles for proof visibility). [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11]

Cross-Referencing and Navigation:

• Enhanced cross-referencing in links.md by adding direct links to theorems and claims, using section anchors for each property, and updating references to point to the new documentation structure. [1] [2] [3]
• Improved navigation by removing the obsolete Properties.md entry and ensuring each property is accessible via its own page.

Minor Codebase Improvements:

• Added missing typeclass instance for HasGovState in EpochState, ensuring consistency in the Agda specification.

These changes make the formal ledger specification more modular, navigable, and maintainable, with each property clearly documented and easily referenced.

Checklist

• Commit sequence broadly makes sense and commits have useful messages
• Any semantic changes to the specifications are documented in CHANGELOG.md
• Code is formatted according to CONTRIBUTING.md
• Self-reviewed the diff

[carlostome]

LGTM!