module module high

`IndisputableMonolith.Mathematics.RamanujanBridge.CongruenceQ3Bridge`

The CongruenceQ3Bridge module establishes that Q₃ contains exactly 12 undirected edges inside the Recognition Science framework. Researchers linking RS graph structures to Ramanujan's congruences would cite this fact. It assembles the claim from imported constants and cost definitions through a collection of supporting lemmas and counts.

claim$Q_3$ has 12 undirected edges.

background

Recognition Science starts from the J-cost functional equation and the time quantum τ₀ = 1 tick supplied by the Constants module. The Cost module supplies the underlying cost and defect measures. CongruenceQ3Bridge forms a submodule of the Ramanujan Bridge, whose parent module states that it supplies the formal bridge between Ramanujan's mathematical structures and Recognition Science.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the edge-count fact required by the parent RamanujanBridge module. That module deciphers Ramanujan's deepest structures inside RS and lists this submodule among its direct imports.

scope and limits

Does not derive values for physical constants such as α or G.
Does not treat directed flux or higher-order congruences.
Does not connect Q₃ to the eight-tick octave or spatial dimension D = 3.

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.Cost module_import

declarations in this module (49)

def Q3_edge_count L59
def directed_flux_Q3 L62
theorem directed_flux_Q3_eq_24 L65
theorem twenty_four_eq_8_times_3 L68
theorem twenty_four_prime_factorization L71
def IsMockOrder L78
theorem mock_orders_are_3_5_7 L81
theorem mock_orders_complete L89
theorem IsMockOrder_iff L102
def IsCongruenceEligible L116
theorem congruence_primes_coprime_24 L119
theorem five_congruence_eligible L124
theorem seven_congruence_eligible L128
theorem eleven_congruence_eligible L132
theorem two_not_congruence_eligible L136
theorem three_not_congruence_eligible L140
theorem thirteen_congruence_eligible L144
theorem three_divides_directed_flux L152
theorem three_not_coprime_24 L156
theorem eleven_exceeds_8tick_bound L160
theorem eleven_congruence_not_mock L164
theorem overlap_is_exactly_5_7 L170
theorem no_cong_prime_between_3_5 L186
theorem no_cong_prime_between_5_7 L193
theorem no_cong_prime_between_7_11 L200
theorem congruence_primes_are_three_smallest L211
theorem offset_5_eq_24_inv_mod_5 L231
theorem offset_7_eq_24_inv_mod_7 L234
theorem offset_11_eq_24_inv_mod_11 L237
theorem congruence_offsets_are_consecutive L240
theorem congruence_offsets_are_flux_inverses L245
theorem congruence_offsets_unique L252
theorem congruence_prime_5_is_phi_discriminant L267
theorem phi_satisfies_quadratic L271
theorem phi_min_poly_discriminant_is_5 L277
theorem congruence_prime_7_is_dft_mode_count L285
theorem nonzero_modes_mod_8 L289
theorem congruence_prime_11_is_passive_edges L294
theorem congruence_primes_Q3_geometric_origins L298
theorem mock_order_bound_is_24_div_3 L310
theorem congruence_eligible_coprime_to_full_flux L313
theorem mock_only_because_divides_flux L322
theorem congruence_only_because_exceeds_bound L328
theorem mock_and_congruence_unified_by_Q3 L345
theorem mock_orders_product L368
theorem congruence_primes_product L371
theorem congruence_product_near_flux_lattice L374
theorem congruence_primes_sum_eq_flux L379
theorem mock_orders_sum_relation L384