gauss_bonnet_Q3
plain-language theorem explainer
The discrete Gauss-Bonnet theorem for the 3-cube states that the total angular deficit summed over its eight vertices equals 4π. Researchers deriving the fine-structure constant from the cubic ledger geometry in Recognition Science would cite this identity. The proof substitutes the vertex count of eight and the per-vertex deficit of π/2 then verifies the arithmetic identity by ring simplification.
Claim. The total curvature of the boundary of the 3-cube equals 4π, computed as the product of the number of vertices (2^D with D=3) and the angular deficit at each vertex: 8 × (π/2) = 4π.
background
The module derives the fine-structure constant from the geometry of the cubic ledger forced by the Meta-Principle. The spatial dimension is fixed at D=3, yielding a cube Q₃ with 2^D vertices, D·2^(D-1) edges and 2D faces. Active edges per tick number one while the remaining eleven are passive field edges. The angular deficit at each vertex is defined as 2π minus the product of faces per vertex and the cube dihedral angle. Upstream, vertices_at_D3 proves the vertex count equals 8 for D=3 and vertex_deficit_eq proves the deficit equals π/2. The module documentation lists this as the first main result: '4π from Gauss-Bonnet: Structural derivation via vertex deficits of Q₃'.
proof idea
The tactic proof obtains (cube_vertices D : ℝ) = 8 by exact_mod_cast from vertices_at_D3. It then rewrites the angular deficit term using vertex_deficit_eq and applies the ring tactic to confirm the identity 8 × (π/2) = 4π.
why it matters
This supplies the total curvature 4π used directly by the downstream theorem solid_angle_Q3_eq to set solid_angle_Q3 = 4 * Real.pi. It realizes the first main result in the alpha derivation module and aligns with the framework landmark D=3 together with the topological identification of ∂Q₃ with S² whose Euler characteristic yields total curvature 4π = 2π · χ(S²).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.