G6 Crystal

-- Orthogenesis/Architecture/G6Crystal.lean · corrected 2026-08-21

-- CORRECTION.  The previous header read "20 facts proved without sorry" and
-- "three open obligations (sorry)".  Both were false, in opposite directions.
-- There was never a `sorry` in this file; the three "obligations" were stated
-- as `True` and discharged by `trivial`, which compiles silently and proves
-- nothing.  A `sorry` at least warns.

/-- The dm³ cycle-threshold count g⁶ = 33 (the monster threshold, 3 × 11).
    Dimensionless: a count of limit cycles, not a frequency, not a length.
    Renamed from `g6_int`, whose docstring called it "the Schumann coupling
    integer" — a name that carried §4's conclusion into the definition it was
    supposed to be independent of. -/
def g6_cycles : ℕ := 33

-- §4  Schumann Resonance Coupling — WITHDRAWN
--
-- Deleted: c_light, R_earth, f4_schumann, schumann_n4_sqrt,
-- g6_within_2pct_of_f4, g6_within_16pct, noise_tol_covers_g6_error.
-- The arithmetic was correct; the physics was not.
--
--   1. UNITS.  g6_cycles = 33 is a dimensionless count.  33.516 is a number
--      of hertz.  |33 - 33.516|/33.516 < 2/100 is a true statement about two
--      reals and an empty one about the world.  The kernel cannot see units.
--   2. WRONG MODE.  33.516 Hz came from f_n = (c/2πR_E)·√(n(n+1)) taken bare —
--      the lossless idealisation, which puts n=1 at 10.59 Hz, not 7.83.
--      ch-schumann-dual, in this same corpus, puts n=4 at 27.30 Hz standard.
--   3. BACK-FITTED CONSTANT.  An A₄:₁ tongue locks at rotation number 4 by
--      definition; 7.83 × 4 = 31.32.  The 4.28 was chosen to reach 33.5.
--   4. NO CAVITY.  Schumann resonance is the Earth–ionosphere cavity.  The
--      Moon has none.  On this deposit's stated application it is absent.
--
-- §2 derives every dimension from g6_cycles and τ alone, so the geometry is
-- untouched.  What the withdrawal costs is the physical justification of
-- 66 = 33·τ.  The geometric justification stands.

-- §9  Obligations — corrected
--
--   S1  arnold_tongue_A4_coupling — DELETED.  It read
--         ∀ δ : ℝ, ‖δ‖ < noise_tolerance → True
--       provable for any hypothesis whatsoever.  Its subject was withdrawn in
--       §4.  A retracted claim does not become an open one, so it is not a
--       `sorry`: marking it so would assert an intention to prove something
--       no longer believed.
--
--   S2  hexagrid_collapse_resistance_superior — DELETED.  It read
--         theorem hexagrid_collapse_resistance_superior : True := trivial
--       The substantive claim — hexagrid beats diagrid on progressive collapse
--       — is an FEM result (Mashhadiali 2013, 2014; Yildirim 2024).  It is
--       empirical.  Lean cannot hold it, and a `sorry` would imply a formal
--       model waiting to be filled in.  It belongs in prose, with its citation.
--
--   S3  coord_coverage — asserted to be tracked in Coverage.lean.  Not
--       verified.  Confirm it is an actual `sorry` before claiming it open.

-- NASAGaps.lean · same date

-- POWER  FN-P-101L · FN-P-402L — REOPENED, no partial credit.
--   FN_P_101L_schumann_proximity re-exported the deleted §4 theorem.
--   FN_P_402L_noise_tolerance restated τ·ε₀ = 2/3 — true of the dm³
--   invariants, silent about power.  Re-exporting a true statement under a
--   gap code does not address the gap; it makes the table look answered.

-- FN-A-104L neighbor traversal — DELETED (vacuous, and redundant).
--   ∀ nb ∈ hexNeighbors h, nb ∈ hexNeighbors h := fun nb hnb => hnb
--   `x ∈ S → x ∈ S`, discharged by the identity function.  True of every set.
--   Not `True`-shaped, so a grep for ": True" or ":= trivial" misses it —
--   the sweep has to be semantic.  FN-A-104L keeps FN_A_104L_reachability.

-- FN-M-302L — REOPENED.  Same tautology, docstringed as "given any two
--   coords in the same colony, there exists a sequence of neighbor steps
--   connecting them".  The statement does not say that.  Nothing else carries
--   this gap.  Closing it needs a reachability relation on HexCoord and a
--   proof that any two coordinates of a connected colony are related by it.

-- What survives, unchanged and non-vacuous:
theorem hex_beats_square : sq_isoperimetric_ratio < hex_isoperimetric_ratio
theorem aspect_ratio_encoded : height_cubits / base_cubits = g6_cycles * 2
theorem height_metres : (height_cubits : ℝ) * cubit_m = 15087.6
theorem nasa_payload_mono : payload_phase01 < payload_phase02
theorem colony_depth2_coords : -- 19 distinct coordinates at depth 2
theorem nasa_gap_closure_summary : -- five gaps, all with real content