passive_edges_at_D3
plain-language theorem explainer
The theorem fixes the passive field edge count of the three-dimensional cube at eleven. Researchers deriving the fine-structure constant from cubic ledger geometry or connecting to Ramanujan pi-series would cite this integer. It follows by direct numerical evaluation of the definition that subtracts one active edge per tick from the twelve total edges.
Claim. For the three-dimensional cube the number of passive field edges equals eleven, where passive field edges are the total cube edges minus the single active edge traversed during each recognition tick.
background
The Alpha Derivation module constructs the fine-structure constant from the geometry of the cubic ledger forced by the meta-principle. The unit cell is the three-cube Q3 with D=3, yielding twelve edges, six faces, and eight vertices. One edge is active per atomic tick while the remaining eleven passive field edges participate in the vacuum coupling and geometric seed.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic difference between cube edges and active edges per tick at D=3.
why it matters
This result supplies the integer eleven that multiplies the four-pi curvature term to form the geometric seed for alpha. It is invoked in the Ramanujan-Deligne exponent theorem, the factorizations of 396 and 9801, the RamanujanPiCert structure, and the passive edge count verification for lepton generations. The count anchors the passive channel in the D=3 geometry of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.