ConservedCharge
plain-language theorem explainer
ConservedCharge equips a type α with a real-valued map that serves as a conserved ledger quantity. ZeroParameterComparisonLedger cites the structure to supply the log-charge field inside the zero-parameter interface for the unconditional inevitability theorem. The declaration is a direct structure definition whose second field is a tautological predicate.
Claim. A structure on a type $α$ consisting of a function $c:α→ℝ$ together with the property that $c(s_1)=c(s_2)$ implies $⊤$ for all $s_1,s_2∈α$.
background
The module introduces the zero-parameter local conserved comparison ledger as the single primitive interface consumed by all downstream emergence theorems. It requires a countable nonempty carrier, an admissible cost, and a conserved scalar quantity called the log-charge. ConservedCharge supplies the third of these requirements. Upstream imports include enumerations of narrative families, kinship systems, and ore classes together with the constant A=1 that records active edges per fundamental tick; none of these are used inside the structure itself.
proof idea
The declaration is a structure definition that directly introduces the charge map and its conservation predicate without further elaboration or lemmas.
why it matters
ZeroParameterComparisonLedger consumes ConservedCharge to complete the primitive ledger object required by the unconditional theorem. The module doc-comment identifies the conserved scalar quantity (log-charge) as one of the five mandatory components of that object. The construction therefore sits inside the Recognition Science ledger interface that feeds hierarchy, factorization, and neutral-dynamics results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.