Gravity Seven Gaps Recognition Ratio Substrate Blocker Nontrivial Source Backed

A family that fills the gap

The declaration nontrivial_source_backed_family_exists is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It answers a specific worry about a proposed derivation. The worry: when the framework tries to derive a ratio bridge from a bare recognition ledger, a discrete record of events, the route might be populated only by trivial examples, like a zero source or a fixed mesh, which would make the derivation hollow. The theorem establishes that this is not the case. It proves that for any nonzero coupling constant and any positive number of channels, there exists a whole family of models, parameterized by a mesh scale, that satisfies the required admissibility conditions. At every nonzero mesh scale, both the geometric deficit and the stationary log-ratio are nonzero, so the family is genuinely populated and not degenerate.

The theorem's content is precise. It states that for a channel count n at least 1 and a nonzero coupling kappa, there exists a recognition ratio family F that is admissible with respect to a source bound and a remainder bound. The source strength is exactly n times the square of the mesh scale, and the product of kappa and the deficit is that same quantity. This is a constructive existence result, not a claim about a specific physical model. It says the conditional positive route, the path that works once a named premise is supplied, has real mathematical substance.

The theorem does not claim that the ratio bridge follows from a bare ledger alone. In fact, the same source file proves the opposite: a bare two-cell ledger cannot distinguish between opposite signed source orientations. A function that tries to recover the signed source from the bare ledger fails universally. The theorem also does not claim that the constitutive coupling it relies on is derived from first principles. The coupling is a definitional model, an extra piece of constitutive data that must be supplied. What the theorem does is show that once that data is given, the derivation is not vacuous: a nontrivial family of models exists to back it.

In plain terms, the declaration fills a gap in a proof strategy. It shows that the strategy is not a dead end for lack of examples. It also draws a sharp line: the extra ingredient, the signed deficit-source coupling, is necessary and cannot be extracted from the bare ledger. This is the honest terminal state of the P2.1 blocker package: the missing premise is named exactly, the positive route is populated, and the negative result is proved.

/-- **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⟩

/-- **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⟩

/-- **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

What this page does not claim

The theorem does not prove that the ratio bridge is derived without an extra constitutive premise. The theorem does not identify the coupling constant kappa with any measured physical quantity. The theorem does not show that the family of models matches any observational data.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioSubstrateBlocker.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: