Gravity Seven Gaps Recognition Ratio Substrate Blocker Sign Blind Bare Ledger Ne

The sign-blind ledger

A recognition ledger is a discrete record of events and their costs. In the Recognition Science framework, a bare ledger records only the cost of each possible event, not the physical mechanism that produced it. The declaration signBlindBareLedger_neg_eq proves a precise limit of that record: for a simple two-event ledger, flipping the sign of a source parameter leaves the entire ledger unchanged. Reversing the orientation of the source produces the same costs, hence the same ledger.

The proof is short and exact. The theorem states that for any real number d, the ledger built from source parameter d equals the ledger built from source parameter -d. Because the two ledgers have identical cost functions, and the remaining fields of a ledger are proofs, the ledgers themselves are equal. This is a THEOREM in the machine-checked library of formal theorems, with no gaps in its derivation.

The consequence is a blocker, not a failure. The framework proves that no function of a bare two-event ledger can universally recover the signed source that produced it. If two opposite sources yield the same ledger, any proposed recovery function would have to output two different values for the same input. The theorem no_bare_ledger_selector_recovers_signed_source states exactly that: no such selector exists. Signed source orientation is extra constitutive data, not information contained in the bare ledger.

This result does not claim that the recognition ratio is unattainable. It claims only that the bare ledger is insufficient. The missing premise is a signed deficit-source constitutive coupling: a source strength equal to a hinge coupling times a geometric deficit, added linearly to the cost action. Once that named premise is supplied, J-stationarity derives the ratio bridge with a cubic remainder, and a nontrivial small-mesh family exists. The bare ledger is blind to sign; the sourced construction sees it.

What this means for the framework: the path from a bare recognition ledger to the recognition ratio requires an additional physical assumption about how sources couple to strain. The theorem does not prove the ratio from the ledger alone, and it does not prove the ratio is impossible. It proves the exact boundary of what the ledger can determine, and points to the specific premise that closes the gap.

/-- **THEOREM (same bare ledger, opposite signed source).** Reversing the
source orientation leaves every J-cost, hence the entire bare recognition
ledger, unchanged. -/
theorem signBlindBareLedger_neg_eq (d : ℝ) :
    signBlindBareLedger (-d) = signBlindBareLedger d := by
  apply recognitionLedger_cost_ext
  funext i j
  rw [show (signBlindBareLedger (-d)).cost i j
      = Cost.Jcost ((twoHingeWitnessBridge (-d)).xRatio i
          / (twoHingeWitnessBridge (-d)).xRatio j) from
        ratioBridgeLedger_cost (twoHingeWitnessBridge (-d)) i j]
  rw [show (signBlindBareLedger d).cost i j
      = Cost.Jcost ((twoHingeWitnessBridge d).xRatio i
          / (twoHingeWitnessBridge d).xRatio j) from
        ratioBridgeLedger_cost (twoHingeWitnessBridge d) i j]
  have hratio :
      (twoHingeWitnessBridge (-d)).xRatio i
          / (twoHingeWitnessBridge (-d)).xRatio j
        = ((twoHingeWitnessBridge d).xRatio i
            / (twoHingeWitnessBridge d).xRatio j)⁻¹ := by
    rw [twoHingeWitnessBridge_xRatio_neg d i,
      twoHingeWitnessBridge_xRatio_neg d j, inv_div_inv, inv_div]
  rw [hratio]
  exact (Cost.Jcost_symm
    (div_pos ((twoHingeWitnessBridge d).xRatio_pos i)
      ((twoHingeWitnessBridge d).xRatio_pos j))).symm

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

/-- **MODEL (the exact premise missing from the bare ledger).**

A signed deficit-source constitutive coupling supplies a channel count, the
hinge coupling and signed geometric deficit, and a source strength satisfying

`sourceStrength sigma = kappa sigma * geometricDeficit sigma`.

It also supplies the positive mesh scale and the structural small-source
bound needed by the cubic estimate.  No field mentions the recognition
ratio or its logarithm. -/
structure DeficitSourceConstitutiveCoupling (H : Type*) where
  channels : ℕ
  channels_pos : 1 ≤ channels
  kappa : H → ℝ
  geometricDeficit : H → ℝ
  sourceStrength : H → ℝ
  source_eq : ∀ σ, sourceStrength σ = kappa σ * geometricDeficit σ
  meshScale : ℝ
  meshScale_pos : 0 < meshScale
  source_dominated :
    ∀ σ, |sourceStrength σ| ≤ (channels : ℝ) * meshScale

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

What this page does not claim

The theorem does not prove that the recognition ratio is impossible to derive. The theorem does not prove that the signed source can be recovered from any richer ledger structure. The theorem does not state that the bare ledger is physically meaningless, only that it is incomplete for this purpose.

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: