Recog Spec Spec

The recognition specification

Recognition Science studies systems that keep a discrete record of events, a ledger. The record is not a free choice: the framework's core theorem forces a particular cost function for recognition, and from that cost a chain of results derives constants and structures. The specification turns that abstract forcing into a concrete, checkable description of what a recognition system must contain and how its units are fixed.

The central object is a pair of anchors: two real numbers that fix a time scale and a length scale. From any such pair, the specification defines a speed as the ratio of the length anchor to the time anchor. The key result is that this calibration is unique: for any ledger and any bridge (the structure connecting two ledgers), there is exactly one set of units that makes the anchors calibrate correctly. The proof is short and relies only on the definition of calibration and the fact that the speed determines the anchors up to an equivalence.

The specification also packages the framework's predictions. It defines default values for the golden ratio φ, the fine-structure-like constant α, mass ratios, and mixing angles, all expressed as powers of φ. It states that an eight-tick pattern exists, that the Born rule holds, and that a universal dimensionless description matches the explicit default. These are not independent assumptions: each is either a definition or a theorem derived from the core forcing chain, and the derivation is recorded.

What the specification establishes in plain language is this: the framework's claims are not a loose collection of guesses. They are a single, closed specification, and the specification is internally consistent. The uniqueness of calibration is the load-bearing result: it says that if you accept the framework's starting point, the units are not adjustable. The speed is fixed by the anchors, and the anchors are fixed up to a scale. That is what makes the framework's constants predictions rather than parameters.

The practical consequence is that the framework can be checked. The specification is written in a machine-checked library of formal theorems, so every step of the derivation is verified by the computer. A reader who wants to know whether the framework's claims hold can inspect the specification directly. The specification does not prove that the framework's starting point is true; it proves that if you accept the starting point, the rest follows.

/-- UniqueCalibration witness for any ledger/bridge/anchors triple. -/
@[simp] lemma uniqueCalibration_any (L : Ledger) (B : Bridge L) (A : Anchors) :
    UniqueCalibration L B A := by
  unfold UniqueCalibration
  use unitsFromAnchors A
  constructor
  · exact unitsFromAnchors_calibrated A
  · intro U hU
    cases U
    simp [Calibrated, unitsFromAnchors, speedFromAnchors] at *
    rcases hU with ⟨rfl, rfl, rfl⟩
    simp

/-- Any two anchor choices calibrating bridges have equivalent speed if
    calibrated from the same ledger. -/
theorem anchors_unique_up_to_units
  (L : Ledger) (B₁ B₂ : Bridge L)
  (A₁ A₂ : Anchors)
  (h₁ : UniqueCalibration L B₁ A₁)
  (h₂ : UniqueCalibration L B₂ A₂)
  (hspeed : speedFromAnchors A₁ = speedFromAnchors A₂) :
  Quot.mk anchorsSetoid A₁ = Quot.mk anchorsSetoid A₂ := by
  have heqv : AnchorsEqv A₁ A₂ := anchors_eq_of_same_speed hspeed
  exact Quot.sound heqv

@[simp] theorem eightTick_from_TruthCore : eightTickWitness :=
  Patterns.period_exactly_8

@[simp] theorem born_from_TruthCore : bornHolds := by
  exact IndisputableMonolith.Verification.TwoOutcomeBorn.TwoOutcomeBornCert.verified_any {}

What this page does not claim

The specification does not prove that the framework's starting point is true; it proves conditional consistency. The specification does not derive the fine-structure constant α; it defines a default value. The anchors are not claimed to be measurable directly; they are a formal device.

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/RecogSpec/Spec.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: