t6_obstruction_closed_framework
plain-language theorem explainer
A closed observable framework need not realize either hierarchy field used by the internal T5→T6 bridge: constant successive ratios along an orbit, or the additive Fibonacci step. Auditors of the T6–T8 spine cite this as the honest obstruction. The proof is a one-line appeal to the combined obstruction theorem in HierarchyRealizationObstruction.
Claim. There exists a closed observable framework $F$ (positive-valued observables $r$, discrete dynamics $T$, nontrivial and closed) and a base state such that the successive ratios $r(T^{k+2}\mathrm{base})/r(T^{k+1}\mathrm{base})$ are not all equal to $r(T^{k+1}\mathrm{base})/r(T^{k}\mathrm{base})$, and also $r(T^{2}\mathrm{base}) \neq r(T\,\mathrm{base}) + r(\mathrm{base})$.
background
This module is the July 2026 T6–T8 spine honesty audit: a machine-checked record of what the repository already proves about its own gaps, without upgrading any tier. Tier tags distinguish THEOREM content from FORCED-CONDITIONAL, MODEL/ENCODING, and OPEN bridges.
A ClosedObservableFramework packages a state space $S$, a dynamics $T:S\to S$, and a positive observable $r:S\to\mathbb{R}$ with nontrivial range, subject to closure (no external input) and finite description (countable states, no continuous moduli). The two hierarchy fields at issue are geometric constancy of successive ratios along an orbit, and the additive step $r(T^{2}s)=r(Ts)+r(s)$ that feeds the quadratic $r^{2}=r+1$ used to force $\varphi$ at T6.
Upstream, closedFramework_does_not_force_realizedHierarchy_fields already states the combined obstruction: the primitive closed layer admits models where both target fields fail. Separate from that obstruction, the audit notes that quadratic uniqueness $r^{2}=r+1\land r>0\Rightarrow r=\varphi$ is available standalone as t6_holds without importing T5.
proof idea
One-line term proof: the declaration is definitionally the same existential as closedFramework_does_not_force_realizedHierarchy_fields from HierarchyRealizationObstruction, so the proof is just that name. No new construction is given here; the audit theorem re-exports the combined obstruction under the T6–T8 spine naming.
why it matters
In the Recognition forcing chain, T6 forces $\varphi$ as the self-similar fixed point of the cost hierarchy. The internal T5→T6 bridge consumes two hierarchy fields (constant successive ratios, and the additive Fibonacci step). This audit theorem records that a bare closed observable framework does not force those fields, so T6 is not free lunch from closure alone.
Downstream it is bundled into t6t8_spine_audit_cert as the t6_obstruction field of the July 2026 honesty certificate, alongside the standalone quadratic algebra fact and the T7/T8 placeholder and linking audits. The module’s stated purpose is not to close the gap but to keep the obstruction visible: any claim that T6 is forced from closed observables without extra structure would contradict this certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.