gate_ledger
plain-language theorem explainer
The gate_ledger definition supplies the fourth necessity gate enforcing ledger structure under J-symmetry. Researchers comparing alternative frameworks cite it when checking that any zero-parameter theory must obey double-entry conservation or else violate the cost foundation. The definition is a direct record construction that marks the gate proven via the separate LedgerForcing module.
Claim. The ledger gate is the record of type NecessityGate with name ``Ledger Forcing'', proven flag true, and violation meaning ``Asymmetric recognition without double-entry conservation''.
background
The inevitability structure module organizes alternatives under a cost-minimization foundation into three buckets and lists six necessity gates that any zero-parameter framework must satisfy. A NecessityGate is the structure with fields name (String), proven (Bool), and violation_meaning (String). The module documentation states the fourth gate explicitly: '4. Ledger Structure: J-symmetry forces double-entry'. Upstream results include the Gate structure from CircuitLedger, which guarantees a DAG topology on parent indices, and the NecessityGate definition itself.
proof idea
This is a definition that constructs the NecessityGate record by direct field assignment: name set to the string 'Ledger Forcing', proven set to true with a comment referencing the LedgerForcing module, and violation_meaning set to the asymmetric-recognition string.
why it matters
The declaration populates the all_gates list that implements the inevitability theorem. It fills gate 4 in the module's enumerated chain, which follows from J-uniqueness (T5) and the Recognition Composition Law. In the broader framework it closes the ledger-forcing step that links cost symmetry to conservation before the phi and dimension gates are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.