from
plain-language theorem explainer
Documents that lifting the full T-1–T8 forcing spine from the additive ledger floor remains an open task, not a finished theorem. Foundation auditors cite it when separating completed forcing steps (T5 J-uniqueness through T8, D=3) from still-unclosed ledger-origin claims. The page records no proof body; the declaration is a status marker inside the public bridge module.
Claim. Deriving the completed T-1 through T8 forcing spine from the additive ledger floor, if that derivation is possible at all, is an open task rather than a finished step of the public foundation chain.
background
The module publishes the theory-only T-1 through T8 forcing spine and stops before private operator or measurement layers. In that spine: T-1 is the absolute distinguishability floor; T0 the Boolean recognition-work split; T1 the cost-form Meta-Principle; T2 two-state discreteness; T3 additive ledger bookkeeping; T4 a recognition witness on the discrete floor; T5 uniqueness of the canonical reciprocal cost $J$; T6 $\varphi$ from self-similar hierarchy; T7 the eight-tick cadence; T8 forces $D=3$.
Upstream fragments point at primitive distinction packaging, one-step trace extension by a distinction act, and the unified chain result that forces $D=3$ with canonical period $8$. The ledger floor is the T3 additive bookkeeping layer on the discrete two-state floor; the open question is whether the whole spine can be recovered from that bookkeeping alone.
proof idea
No proof body is supplied (zero body lines). The declaration functions as an explicit non-completion marker: it states that a derivation from the ledger floor is not claimed. There is no tactic script, term proof, or one-line wrapper to walk. Readers should treat neighboring completed bridges (T-1 to T0, T0 to T1, and the unified T5–T8 chain) as the actual proved steps, not this marker.
why it matters
Keeps the public foundation honest about the boundary between proved forcing (especially T5 $J$-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$ in the unified chain) and ledger-origin closure that is still open. Downstream action-layer results (cost-rate Euler–Lagrange at the constant path 1, pointwise convexity of $J$, local-to-global minima for the action, Hamilton equations from EL) depend on the completed cost and ledger apparatus, not on a finished ledger-floor derivation of the whole spine. The marker prevents over-claiming that T3 bookkeeping alone already yields the full T-1–T8 package inside this repository.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.