ForcedClosure
plain-language theorem explainer
Packages the three combinatorial invariants of the 3-cube that RS free-energy closure actually pins: cycle rank b₁ = 5, gauge-invariant link count equals that rank, and passive seed-channel count 11 ≠ 5. Parametrized by the U(1) kinetic normalization κ_γ but independent of it. Downstream irreducibility theorems cite it as the κ-blind side of the α⁻¹ scaling test. Pure definition: a three-conjunct Prop on ℕ equalities.
Claim. For every real $\kappa$, the forced-closure predicate at $\kappa$ is the conjunction of three facts on the 3-cube $Q_3$: the U(1) cycle rank equals $5$; cube edges minus gauge redundancy equals that cycle rank; and the passive field-edge count is not equal to the cycle rank. The parameter $\kappa$ does not appear in any conjunct.
background
The module upgrades α⁻¹ from a measured boundary datum to a structural irreducibility theorem via the κ_γ-scaling test. Insert a free positive U(1) kinetic normalization so that α⁻¹(κ) = κ · α⁻¹; then ask whether any forced RS closure condition can pin κ (equivalently pin α⁻¹).
Spatial dimension is fixed at D = 3 (T8/T9). The 3-cube has cube_edges(D) = D · 2^(D-1) = 12 edges and 8 vertices. The cycle rank (first Betti number of the 1-skeleton) is b₁ = E − V + 1 = 5, also written cube_cycle_rank. Gauge redundancy is V − 1 = 7 phases. Passive field edges are total edges minus the active edge per tick, giving 11 for D = 3: the seed channel count.
These three Nat statements are the genuine combinatorial/topological invariants the free-energy closure on Q₃ pins. None mentions κ_γ. The Gaussian log-det and Green-diagonal numerics (module doc) likewise fail to produce a counterterm that would fix the kinetic normalization.
proof idea
Definition, not a proved theorem. The body is the three-way conjunction
cube_cycle_rank = 5 ∧ (cube_edges D − gauge_redundancy = cube_cycle_rank) ∧ (passive_field_edges D ≠ cube_cycle_rank).
The dummy binder _κ makes the predicate a function ℝ → Prop so it can sit in the same interface as κ-dependent closures, while the right-hand side never mentions κ. Discharge of the three conjuncts is deferred to forcedClosure_holds, which applies the upstream equalities cube_cycle_rank_eq_5, physical_link_dof_eq_cycle_rank, and seed_channel_count_ne_gauge_dof.
why it matters
Load-bearing interface for the κ_γ-irreducibility theorem. Parent results that consume it:
forcedClosure_holds: the three facts hold for every real κ.forcedClosure_kappa_independent: ForcedClosure κ ↔ ForcedClosure κ' by reflexivity.alphaInv_irreducible_under_closure: for any target t > 0 there is κ > 0 with ForcedClosure κ and α⁻¹(κ) = t.alpha_not_pinned_by_forcedClosure: the Pins predicate fails, so closure does not select a unique α⁻¹.forcedClosure_plus_blind_conjunct_cannot_pinandalphaInvK_meets_band: stability and band-intersection corollaries.
Framework role: contrasts with derived constants such as ℏ = φ⁻⁵. The inverse fine-structure coupling remains a free U(1) kinetic normalization (renormalization-scheme input), not a forced RS output. Ties to T8 (D = 3) and the eight-tick/Q₃ geometry that supplies b₁ = 5 and the seed count 11. Closes the panel's IRREDUCIBLE branch of the σ = 0 closure computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.