ModularDiscriminantBridge
plain-language theorem explainer
The structure records that the exponent 24 in the modular discriminant equals the directed edge count on the three-dimensional hypercube. Researchers reinterpreting the Ramanujan tau function or bosonic string dimensions in discrete physics would cite this equality to replace extra-dimensional counting with flux degrees of freedom. The definition sets the default exponent to 24 and verifies the match by reflexivity against the directed edge count function.
Claim. The structure asserts a natural number exponent equal to 24 together with the equality that this exponent matches twice the number of edges in the three-dimensional hypercube.
background
The module sets the number 24 as the count of directed flux degrees of freedom on the Q3 ledger. The upstream directed_edge_count definition states that each undirected edge becomes two directed edges because J-symmetry requires reciprocal flows in both orientations, yielding 2 times cube_edges(d) and exactly 24 when d equals 3. The eta_exponent result from the cosmology module supplies the observed value of the Dedekind eta function for comparison with powers of phi. The module document replaces the string-theory reading of 24 transverse dimensions with the double-entry ledger count forced by the eight-tick octave and D equals 3.
proof idea
The structure is introduced with eta_exponent defaulting to 24 and the matches_flux field discharged by reflexivity, which directly equates the constant to the output of directed_edge_count on the dimension parameter.
why it matters
This definition supplies the certificate linking the modular discriminant exponent to the directed flux count and feeds the downstream modularDiscriminantBridge instantiation. It closes the identification of 24 with twice the edges of Q3, consistent with the forcing chain step that fixes D equals 3 and with the double-entry principle. The module document notes that this accounts for the Leech lattice dimension without extra spacetime dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.