ConservationCert
This structure packages three numerical assertions that exactly five conservation laws exist in the RS framework, three of them arising from spacetime symmetries. A physicist deriving Noether theorems from RS symmetries would cite it to confirm the count matches the expected D=3 plus two additional laws. The definition simply assembles the cardinality of the inductive type ConservationLaw with the constant spacetimeConserved and the arithmetic relation that closes the total at five.
claimLet $L$ be the finite type whose elements are the five conservation laws (energy, momentum, angular momentum, electric charge, baryon number). The structure asserts that the cardinality of $L$ equals 5, that the number of spacetime-conserved quantities equals 3, and that this number plus 2 equals 5.
background
The module states that Noether's theorem maps each symmetry to a conservation law and lists the RS conserved quantities: recognition charge conservation (σ = 0), total J decreasing (second law), momentum, angular momentum, and energy. Five canonical laws are identified with configDim D = 5. ConservationLaw is the inductive type whose five constructors are exactly these laws. spacetimeConserved is the constant definition equal to 3, corresponding to the three spacetime symmetries in D = 3 dimensions.
proof idea
This is a structure definition that directly encodes the three equalities. No tactics or lemmas are applied; the fields simply record the cardinality of the inductive type ConservationLaw, the value of spacetimeConserved, and the arithmetic identity that their sum closes at five.
why it matters in Recognition Science
The structure supplies the concrete certificate consumed by the downstream definition conservationCert, which instantiates it with the computed counts. It therefore closes the bookkeeping step that links the five-law count to the framework landmark D = 3 and the five canonical laws listed in the module documentation.
scope and limits
- Does not derive the explicit forms or charge assignments of the five laws.
- Does not prove that the listed laws are conserved under RS dynamics.
- Does not address interactions or closure properties beyond the total count.
- Does not extend to additional conservation laws outside the five enumerated.
formal statement (Lean)
40structure ConservationCert where
41 five_laws : Fintype.card ConservationLaw = 5
42 three_spacetime : spacetimeConserved = 3
43 total_five : spacetimeConserved + 2 = 5
44