passive_field_edges
plain-language theorem explainer
Passive field edges count the non-transition edges in a d-dimensional hypercube that dress the recognition interaction. Researchers deriving the fine-structure constant from cubic ledger geometry cite this to isolate the factor of 11 at D=3. The definition is a direct subtraction of the fixed active edge count of one from the closed-form hypercube edge total.
Claim. The passive field edge count is given by $E(d) := d · 2^{d-1} - 1$, subtracting the single active edge traversed per atomic tick from the total hypercube edges.
background
The Alpha Derivation module constructs α^{-1} from the geometry of the unit cube Q_3 in the discrete ledger. For D=3 the cube has 12 edges total. One edge is traversed per atomic tick, leaving the passive field edges to mediate the coupling to the vacuum. The module doc states that these passive edges dress the interaction and supply the factor 11 to the geometric seed 4π × 11.
proof idea
One-line definition that subtracts the constant active_edges_per_tick from the result of cube_edges d.
why it matters
This supplies the integer 11 that multiplies the solid angle in the geometric seed, feeding directly into alpha_seed_structural and geometric_seed_factor. It is invoked in mass anchor theorems such as B_pow_Lepton_eq and E_passive. The definition realizes the active/passive split required by the eight-tick octave and D=3 in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.