module module high

`IndisputableMonolith.Mathematics.RamanujanBridge.DirectedFlux24`

This module defines directed edges on the Q₃ cubic lattice as oriented pairs connected by unit cube steps and computes their counts along with related equalities. It links the resulting directed flux to the 24-dimensional Leech lattice. Researchers bridging Ramanujan's structures to Recognition Science would cite these constructions to ground higher-dimensional geometry in the cubic ledger. The module consists of type definitions, count functions, and direct equalities.

claimA directed edge on the $Q_3$ lattice is an oriented pair $(s,t)$ with $s,t$ in the integer lattice and $1$-norm distance exactly $1$. The module defines the directed edge count on $Q_3$, proves it equals twice the undirected count, and equates this flux to the Leech lattice dimension of $24$.

background

The module sits inside the Ramanujan Bridge and draws on the cubic ledger from AlphaDerivation, where vertex deficits on $Q_3$ produce $4π$ via Gauss-Bonnet. It uses the RS time quantum τ₀ = 1 tick from Constants. DirectedEdge is introduced as an oriented pair (source, target) connected by a cube edge on the $Q_3$ lattice, with supporting counts edges_QD and edges_Q3.

proof idea

This is a definition module, no proofs. It introduces the DirectedEdge type, defines edge counts for QD and Q3, states the equality directed_edges_eq_double_entry, and records the equality leech_dimension_eq_directed_flux relating the count to dimension 24.

why it matters in Recognition Science

This module supplies the directed flux and Leech reinterpretation that feed the RamanujanBridge module. It supplies the geometric link from the Q₃ cubic ledger to the 24-dimensional Leech lattice inside the broader decipherment of Ramanujan's mathematics by Recognition Science.

scope and limits

Does not derive numerical edge counts or explicit values.
Does not extend definitions beyond the Q₃ cubic lattice.
Does not address modular forms or other Ramanujan functions.
Does not connect to physical constants or forcing chain steps.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Mathematics.RamanujanBridge module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import

declarations in this module (15)

structure DirectedEdge L66
theorem edges_QD L75
theorem edges_Q3 L78
def directed_edge_count L85
theorem directed_edges_Q3 L95
theorem directed_edges_eq_double_entry L99
structure ModularDiscriminantBridge L112
def modularDiscriminantBridge L119
def leech_lattice_dimension L128
theorem leech_dimension_eq_directed_flux L130
structure DimensionalReinterpretation L146
def dimensionalReinterpretation L163
theorem tau_2_coefficient L172
theorem ramanujan_deligne_exponent L182
theorem twenty_four_decomposition L188