edgeDualCount
plain-language theorem explainer
edgeDualCount defines the dual edge count as twice the cube edge count, yielding 24. Physicists deriving CKM mixing angles from Recognition Science ledger geometry cite it to fix the V_cb coupling at 1/24. The definition is a direct arithmetic wrapper around the upstream cubeEdges constant.
Claim. The edge-dual count is defined as $2$ times the number of edges of the unit cube, which equals 24.
background
The RSBridge module derives CKM mixing angles from geometric couplings in the Recognition ledger rather than arbitrary parameters. Upstream, cubeEdges is defined as 12 in FreudenthalTriangulationCert, ParticlePhysicsGenerationsFromRS, and the local RSBridge file, with documentation stating it is the unit cube edge count. The module doc states that V_cb equals 1/24 from the edge-dual coupling, where 24 equals 2 times 12 edges of the cube dual.
proof idea
This is a one-line definition that multiplies the cubeEdges constant by 2.
why it matters
This supplies the geometric count used in edgeDualCount_eq to prove equality to 24 and in mixingAngles_geometric_origin to derive V_cb = 1/24. It also populates the edgeDual field of the RSBridge structure. The definition realizes the module claim that mixing angles arise from ledger geometry, consistent with the eight-tick octave and D = 3 in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.