Constants Consistency Consistency Status

A status report, not a proof

The consistency_status declaration is a short text string that acts as a status report for the Recognition Science framework's constants. It lists the checks that have been performed on the definitions of fundamental quantities like the tick duration and the golden ratio. Think of it as a checklist that confirms certain internal definitions agree with each other and with externally calibrated values.

The report confirms three things. First, it defines tau0_SI, the duration of one fundamental tick in seconds, using standard physical constants. Second, it verifies that this SI-based value matches the framework's own dimensionless definition of the tick. Third, it confirms that the golden ratio is defined consistently across different modules of the framework's machine-checked library of formal theorems.

What the status report does not do is prove any physics. It is a definition, not a theorem. It does not claim that the framework's constants are correct, only that they are internally consistent and that one of them has been converted to SI units for comparison with experiments. The actual derivation of these constants from first principles is a separate matter, established elsewhere in the framework's library.

In Recognition Science, this distinction matters. The framework distinguishes between what is proved, what is defined, and what is merely checked for consistency. The consistency_status declaration belongs squarely in the defined and checked category. It is a useful bookkeeping tool, but it carries no physical content of its own.

def consistency_status : String :=
  "✓ tau0_SI defined as SI-calibrated tick duration\n" ++
  "✓ tau0_SI_eq_derivation: matches Derivation.tau0\n" ++
  "✓ tau0_SI_pos: is positive\n" ++
  "✓ phi_consistency: φ matches across modules\n" ++
  "\n" ++
  "NOTE: RS-native units (Foundation.tick = 1) are dimensionless.\n" ++
  "SI values (tau0_SI) are for external calibration only."

/-- The τ₀_SI matches Derivation.tau0. -/
theorem tau0_SI_eq_derivation : tau0_SI = Derivation.tau0 := by
  unfold tau0_SI Derivation.tau0
  rfl

/-- The golden ratio φ is defined consistently across modules. -/
theorem phi_consistency :
    Constants.phi = IndisputableMonolith.Constants.phi := rfl

What this page does not claim

The consistency_status declaration does not prove that the framework's constants are physically correct. It does not derive the values of the constants from first principles. It does not claim that the SI-calibrated tick duration has been experimentally verified.

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/Constants/Consistency.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: