gate_dimension
plain-language theorem explainer
The gate_dimension definition records the sixth necessity gate in the inevitability structure, asserting that any cost-minimizing framework must force exactly three spatial dimensions or admit non-trivial linking violations. Researchers checking alternative gravity or higher-dimensional models against Recognition Science would cite this gate when testing the zero-parameter claim. The definition is a direct record construction that flags the gate as unproven scaffolding pending a linking argument tied to the gap-45 derivation.
Claim. Let $G_6$ be the necessity gate with name ``D = 3 Forcing'', proven flag false, and violation meaning ``Non-trivial linking in $D ≠ 3$''.
background
The InevitabilityStructure module organizes alternatives under the cost-minimization foundation into three buckets and lists six necessity gates that any zero-parameter framework must violate. NecessityGate is the structure that records each gate's name, proof status, and the physical consequence of violation. Gate 6 specifically encodes the dimension claim: linking requirements derived from the Recognition Composition Law force $D=3$. Upstream results supply the NecessityGate structure itself plus the gap definitions that appear in the phi-ladder mass formulas and the Gap45 derivation.
proof idea
One-line record constructor that directly populates the three fields of NecessityGate with the dimension claim and explicitly sets proven to false to mark the scaffold.
why it matters
This gate completes the enumeration inside all_gates, which collects the six choke points any alternative theory must break. It corresponds to T8 of the forcing chain (eight-tick octave plus self-similarity imply $D=3$). The open question it touches is the explicit linking theorem that would discharge the scaffold and set proven to true.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.