admissible
plain-language theorem explainer
The admissible predicate declares every local ledger state admissible for the information-theoretic Landauer bound. Researchers working on cost-rate Euler-Lagrange equations and geodesic paths would cite this when restricting to admissible inputs in the action functional. The definition is a one-line wrapper that unconditionally sets the predicate to True.
Claim. For every minimal local ledger state $s$ (a finite set of active bonds with positive real multipliers), the predicate admissible$(s)$ holds.
background
Module Information.Thermodynamics formalizes the relationship between Recognition Science cost and thermodynamic entropy, anchoring the theory in the Landauer limit under the eight-tick dissipation setting. LedgerState is the structure with fields active_bonds : Finset ℕ, bond_multipliers : ℕ → ℝ and the axiom bond_pos ensuring positivity on active bonds; total recognition cost is defined over those bonds. Upstream LedgerState variants appear in VariationalDynamics (conserved log-ratio charge) and InformationIsLedger (finite collection of recognition events), while A from IntegrationGap supplies the active edge count per tick.
proof idea
One-line definition that sets the predicate to True for any input LedgerState.
why it matters
This supplies the admissibility condition required by downstream results in Action.EulerLagrange (const_one_is_geodesic, costRateEL_const_one, costRateEL_implies_const_one) and Action.FunctionalConvexity (actionJ_convex_on_interp, actionJ_local_min_is_global). It anchors the local information ledger inside the Landauer bound module, connecting to the eight-tick octave and D = 3 from the forcing chain. It touches the open question of whether non-trivial constraints will later be imposed for specific dissipation bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.