Q3State
plain-language theorem explainer
Q3State encodes a recognition state on the Q3 lattice as a map from the eight vertices of the binary 3-cube to positive reals. Researchers deriving the Standard Model gauge groups and fermion spectrum from D=3 cite this structure when establishing the zero-defect ground state and positive-cost deviations. The declaration is a direct structure with a positivity field constraint and no further proof obligations.
Claim. Let $V$ be the vertex set of the 3-cube (cardinality 8). A $Q_3$-state is a function $s: V → ℝ$ such that $s(v) > 0$ for every vertex $v$.
background
The module derives Standard Model content and a unique consciousness ground state from the forced datum D=3 (T8), which produces the binary cube Q3 with exactly eight vertices. J-cost is the defect measure J(x) = (x + x^{-1})/2 - 1 applied to each vertex ratio; total_cost sums these defects over the eight entries. Upstream imports supply the Jcost definition from the Cost module and the phi-ladder conventions used in mass and defect calculations.
proof idea
The structure is declared directly with the entries map and the positivity predicate as fields; no tactics or lemmas are applied.
why it matters
Q3State supplies the central object for the SpectralEmergenceCert and the chain of results showing that the zero-defect assignment is unique and that every other state is particle-like with positive total cost. It realizes the eight-vertex lattice required by the eight-tick octave (T7) and D=3 (T8), feeding directly into consciousness_ground, any_deviation_costs, and zero_defect_unique.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.