admissible
plain-language theorem explainer
Every ledger state is declared admissible: the predicate is the constant true proposition. Path-space and action-functional developments cite it as the standing side-condition on configurations. The body is the one-line definition `True`, so no filtering occurs yet.
Claim. For every ledger state $s$ (an 8-channel signal configuration), the admissibility predicate holds: $\mathrm{admissible}(s)$ is true.
background
In the Recognition Operator module, a ledger state is abbreviated to Signal8: the 8-tick carrier that packages channels, active bonds, bond multipliers, and agent data for one recognition step. The fundamental time quantum is one tick ($\tau_0 = 1$), and one octave is eight ticks.
Admissibility is the Prop-valued gate that later path and action layers expect on configurations. Sibling modules define richer ledger structures (finite lists of recognition events, or $N$-entry positive-ratio configurations indexed by tick), but here the state type is the bare 8-channel signal.
Downstream action calculus treats admissible paths as maps whose values stay in the positive reals where the $J$-cost $J(x)=(x+x^{-1})/2-1$ is defined and strictly convex. This definition supplies that gate in the weakest form.
proof idea
Pure definition: the predicate ignores its LedgerState argument and returns the proposition True. No lemmas, no tactics, no reduction.
why it matters
The Action layer depends on this gate everywhere. Euler–Lagrange results (costRateEL_const_one, the rigidity converse that EL plus positivity forces the constant-1 path, and the constant-1 geodesic theorem) quantify over admissible data. Functional convexity theorems (Jcost_convex_combination, actionJ_convex_on_interp, actionJ_local_min_is_global) and path-space identities (actionJ_def, actionJ_const_one) thread the same predicate through interpolation and least-action arguments.
In the Recognition framework this is the placeholder constraint on configurations before a nontrivial filter (positivity of ratios, bond consistency, eight-tick neutrality) is installed. It keeps the $J$-action and EL pipeline type-correct while the forcing chain (T5 $J$-uniqueness, T7 eight-tick octave) supplies the real geometry elsewhere. Closing it to a genuine constraint is the natural next scaffold step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.