ConservationLaw
The inductive type enumerates five conserved quantities in Recognition Science: energy, momentum, angular momentum, electric charge, and baryon number. Physicists applying Noether correspondences to RS symmetries cite it to equate three spacetime-derived laws with D = 3 and total laws with configDim = 5. The definition is a direct inductive enumeration that derives Fintype for immediate cardinality checks.
claimThe set of conservation laws consists of energy, momentum, angular momentum, electric charge, and baryon number.
background
Recognition Science obtains conservation laws from symmetries via Noether's theorem. The module lists five canonical laws, three arising from spacetime symmetries (energy from time translation, momentum from spatial translation, angular momentum from rotation) and two internal charges (electric charge, baryon number), matching configDim D = 5. The upstream Ledger structure defines a general conservation law as a named charge assignment charge : α → ℤ together with a closure condition that any interaction list has net zero charge.
proof idea
The declaration is an inductive definition with five constructors. It derives DecidableEq, Repr, BEq, and Fintype in one step to support downstream cardinality and equality proofs.
why it matters in Recognition Science
This supplies the concrete enumeration required by ConservationCert to assert Fintype.card = 5, spacetimeConserved = 3, and total five laws. It realizes the module claim that five laws equal configDim D = 5 with three from spacetime symmetries per T8. It also feeds conservationLawCount and the trivial charge example in Ledger.
scope and limits
- Does not assign explicit charge maps to each law.
- Does not prove closure or conservation properties.
- Does not derive the laws from explicit symmetries.
- Does not reference J-cost, phi-ladder, or RCL.
formal statement (Lean)
27inductive ConservationLaw where
28 | energy | momentum | angularMomentum | electricCharge | baryonNumber
29 deriving DecidableEq, Repr, BEq, Fintype
30