module module

`IndisputableMonolith.Unification.QuantumGravityOctaveDuality`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

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

IndisputableMonolith.Unification.SpacetimeEmergence 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 (41)

theorem jcost_eq_sq_div L77
theorem jcost_nonneg_amgm L84
theorem jcost_zero_iff_one L89
theorem gm_pair_unity L100
theorem jcost_is_amgm_gap L105
theorem jcost_reciprocal_symmetry L113
theorem kappa_hbar_octave L129
theorem hbar_kappa_octave L140
theorem kappa_per_octave_eq_inv_hbar L146
theorem hbar_eq_eight_div_kappa L151
theorem kappa_eq_eight_div_hbar L156
theorem phi_fifth_self_dual L161
lemma phi5_mul_phi5 L165
theorem kappa_fibonacci_form L172
theorem hbar_fibonacci_form L181
theorem kappa_hbar_fibonacci_consistency L190
lemma G_eq_inv_pi_hbar L202
theorem G_eq_phi_fifth_over_pi L208
theorem G_hbar_gauss_bonnet L217
theorem G_hbar_pos L222
theorem G_fibonacci_form L226
theorem kappa_per_octave_eq_G_pi L237
theorem G_pi_eq_phi5 L242
theorem planck_area_eq_inv_pi L256
theorem planck_area_pos L261
theorem G_over_hbar_phi_tenth L267
theorem hbar_over_G L277
theorem kappa_G_product L289
theorem phi_fibonacci_recursion L307
theorem fibonacci_mass_recursion L320
theorem mass_ratio_is_phi L325
theorem fibonacci_triple_sum L331
theorem mass_ladder_strictly_increasing L336
theorem phi_pow_fibonacci_sum_le L346
structure QGOctaveCert L359
def qg_octave_cert L389
theorem qg_octave_cert_inhabited L405
theorem three_products L412
theorem G_pi_eq_inv_hbar L422
theorem octave_duality_witness L428
theorem phi5_is_both_quantum_and_gravitational L443