Gravity Seven Gaps Recognition Ratio Substrate Blocker

/-- **P2.1 HEADLINE THEOREM (strongest honest terminal).**

The exact missing premise preventing `recognition_ratio_derived` from the
bare `RecognitionLedger` is `DeficitSourceConstitutiveCoupling`: a signed
source `c_sigma = kappa_sigma * delta_sigma` linearly coupled to total
strain in the J-cost action.  Coboundary circulation gives zero, an imposed
budget is circular, and the bare J-ledger cannot choose between opposite
source orientations.  With that named premise supplied, J-stationarity
derives the ratio bridge, and a nontrivial uniform source-backed family
exists. -/
theorem recognition_ratio_derived_bare_ledger_terminal :
    RecognitionRatioSubstrateBlockerCertificate where
  coboundary_cycle_telescope := by
    intro Λ s hs v m hcycle
    exact closedCycle_coboundary_sum_eq_zero hs v m hcycle
  imposed_budget_is_circular := by
    intro n t kappa delta hbudget
    exact budget_implies_ratio_without_stationarity t kappa delta hbudget
  bare_ledger_cannot_recover_signed_source :=
    no_bare_ledger_selector_recovers_signed_source
  coupling_derives_ratio := by
    intro H C σ
    exact recognition_ratio_derived_of_deficit_source_coupling C σ
  nontrivial_source_family := by
    intro n hn h₀ kappa hκ
    exact nontrivial_source_backed_family_exists n hn h₀ kappa hκ

/-- **THEOREM (the exact bare-ledger blocker).** No function of a bare
`RecognitionLedger (Fin 2)` can universally recover the signed source of
the exact unit-coupled witness family.  The ledgers at sources `1` and `-1`
are equal, while the required outputs are different.  Therefore signed
deficit-source orientation is extra constitutive data, not information
contained in the bare ledger. -/
theorem no_bare_ledger_selector_recovers_signed_source :
    ¬ ∃ select : RecognitionLedger.RecognitionLedger (Fin 2) → ℝ,
      RecoversSignedSourceFromBareLedger select := by
  rintro ⟨select, hselect⟩
  have hneg := hselect (-1)
  have hpos := hselect 1
  rw [signBlindBareLedger_neg_eq 1] at hneg
  norm_num at hneg hpos
  linarith

/-- **THEOREM (the conditional `recognition_ratio_derived`).** Once the
named deficit-source constitutive coupling is supplied, J-stationarity
derives the bridge relation with explicit remainder constant `n / 6`.
No hypothesis states a fact about `xRatio` or `log xRatio`. -/
theorem recognition_ratio_derived_of_deficit_source_coupling {H : Type*}
    (C : DeficitSourceConstitutiveCoupling H) (σ : H) :
    |Real.log ((ratioBridgeFromDeficitSourceCoupling C).xRatio σ)
        - C.kappa σ * C.geometricDeficit σ|
      ≤ (C.channels : ℝ) / 6 * C.meshScale ^ 3 :=
  (ratioBridgeFromDeficitSourceCoupling C).ratio_relation σ

/-- **THEOREM (nontrivial source-backed family).** For every nonzero
coupling and positive channel count, the quadratic sourced family is
uniformly admissible.  Its source is exactly `n*h^2`, and at every nonzero
mesh both its geometric deficit and stationary log-ratio are nonzero.
Thus the conditional positive route is populated by a genuine small-mesh
family rather than a zero-source or fixed-mesh witness. -/
theorem nontrivial_source_backed_family_exists
    (n : ℕ) (hn : 1 ≤ n) (h₀ kappa : ℝ) (hκ : kappa ≠ 0) :
    ∃ F : RecognitionRatioFamily,
      F.IsAdmissible h₀ kappa ((n : ℝ) / |kappa|)
          ((n : ℝ) * h₀ ^ 3 / 6) ∧
      (∀ h, kappa * F.deficit h = (n : ℝ) * h ^ 2) ∧
      (∀ h, h ≠ 0 →
        F.deficit h ≠ 0 ∧ 0 < Real.log (F.ratio h)) := by
  refine ⟨quadraticSourceFamily n kappa,
    quadraticSourceFamily_isAdmissible n hn h₀ kappa hκ, ?_, ?_⟩
  · intro h
    show kappa * ((n : ℝ) / kappa * h ^ 2) = (n : ℝ) * h ^ 2
    field_simp
  · intro h hh
    exact ⟨quadraticSourceFamily_deficit_ne_zero n hn kappa h hκ hh,
      quadraticSourceFamily_logRatio_pos n hn kappa h hκ hh⟩