Realization Calculus

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Included manuscript sections

• current_scope.tex

Read the typeset paper

1 \section{Formal coverage and computational scope}\label{sec:edition-scope}
2 This chapter develops common refinements, complete filtered inversion, lattice gluing, rectangular Smith congruences, and analytic and multilevel defects. It also includes the specializations, finite graph construction, worked realizations, and three algorithm specifications associated with the foundational formal contract.
3 
4 \input{generated/current_scope.tex}
5 
6 The inherited Lean contract has 25 rows: 21 canonical numbered items, one Smith-phase identity, and three algorithm specifications. That foundational contract has its own source identity and scope. The chapter-wide correspondence separately records the exact statements, proof targets, source hashes, and execution evidence. A row may use several declarations, and several source labels may refer to one written theorem. These are distinct counting units.
7 
8 The source archive preserves the foundational sources and their reports. Each verification record applies only to the source hashes and statement scopes it identifies. An earlier preservation report does not certify subsequently edited text.
9 
10 The worked plates give exact models. The formal companion in the back matter explains the chapter-wide proof scope and the foundational declaration-level contract. Illustrations and finite checks support understanding and implementation. Universal claims depend on their written proofs and the exact formal statements where coverage is recorded.
11 
12 The twenty-four worked plates follow this account of the proof scope. Their statement references identify the mathematical text of Chapter II.

Back to source controls

Back to Realization Calculus