balanced_floor_recognition_source_balance
plain-language theorem explainer
The minimal balanced-floor recognition witness stores its balance hypothesis as an explicit source-balance field, and that field equals the input by definition. Anyone wiring the absolute-floor (T-1) certificate into the T4 recognition step cites this projection. The proof is pure reflexivity on the structure constructor.
Claim. Let $C$ be the Boolean recognition-work cost with $C(\mathsf{false})=0$ and $C(\mathsf{true})=1$. Given a balance hypothesis $h$ asserting $C(\mathsf{false})=0$, the source-balance component of the minimal balanced-floor recognition witness built from $h$ is definitionally equal to $h$.
background
The Unified Forcing Chain module shows that T0 through T8 are forced from the cost foundation (Recognition Composition Law plus normalization and calibration). The absolute floor (T-1) is the Boolean configuration space on which a concrete recognition-work cost lives: cost zero on false and one on true.
A balanced-floor recognition witness packages two pieces: the balance hypothesis that the floor cost of false vanishes, and a minimal recognition pair (false, false). Upstream, balanced_floor_recognition builds exactly that structure by setting the source-balance field to the input hypothesis and the recognition field to that pair.
This declaration sits at the T-1/T4 interface: the module notes that T4 (Recognition) follows from the discrete floor and the floor ledger. The source-balance field is the explicit certificate that the floor is already balanced before recognition is read off.
proof idea
One-line reflexivity. The upstream constructor of the balanced-floor recognition witness defines the source-balance field to be the input hypothesis hbalanced. Projecting that field and comparing to hbalanced is therefore definitional equality, discharged by rfl.
why it matters
Keeps the absolute-floor balance certificate first-class rather than buried inside an opaque proof term. In the forcing chain, T-1 (absolute floor) is the meta-language precondition that makes the rest of the spine statable; T4 (Recognition) is read from the discrete floor plus the floor ledger. This lemma is the bookkeeping step that recovers the balance source from the minimal recognition witness, so later steps can cite a named equality instead of unfolding the structure by hand.
No downstream dependents are recorded yet in the graph. Framework landmarks touched: the absolute-floor end of the T-1 to T8 inevitability chain, and the handoff into T4 Recognition. It does not itself force J-uniqueness (T5), phi (T6), the eight-tick octave (T7), or D=3 (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.