ConservedCharge
A structure on any type α supplies a real-valued charge map together with a predicate that equal charges satisfy a true statement. Researchers constructing the zero-parameter comparison ledger for the unconditional inevitability theorem cite this as the conserved scalar component. The declaration is a direct structure definition with two fields and no proof body.
claimLet α be a type. A conserved charge on α consists of a function q : α → ℝ together with the assertion that ∀ s₁, s₂ ∈ α, q(s₁) = q(s₂) implies ⊤.
background
Module LedgerCanonicality introduces the zero-parameter local conserved comparison ledger as the core interface for emergence theorems. The ledger packages a countable nonempty carrier, an admissible cost function, and a conserved scalar quantity called the log-charge. The ConservedCharge structure supplies this scalar component. Upstream results include the active edge count A from IntegrationGap, satisfying the φ-power balance identity at D = 3.
proof idea
The declaration is a structure definition. It introduces the charge map and the conservation predicate as fields with no lemmas or tactics applied.
why it matters in Recognition Science
This structure supplies the charge field required by the parent ZeroParameterComparisonLedger, which packages the full primitive for downstream hierarchy and factorization theorems. It realizes the conserved scalar quantity listed among the five components in the module documentation. In the Recognition framework it supports the forcing chain by providing a conserved quantity compatible with self-similar dynamics.
scope and limits
- Does not specify any functional form or scaling for the charge map.
- Does not derive the conservation predicate from dynamics or cost functions.
- Does not constrain the charge values to a particular interval or lattice.
formal statement (Lean)
38structure ConservedCharge (α : Type) where
39 charge : α → ℝ
40 charge_conserved : ∀ (s₁ s₂ : α), charge s₁ = charge s₂ → True
41
42/-- A zero-parameter local conserved comparison ledger packages all the
43primitive structure needed for the unconditional theorem. -/