Relativity Ilg Params

The parameter record

In the Recognition Science framework, relativity ilg params defines a minimal parameter record. The record holds two real numbers: alpha, which defaults to 1, and Clag, which defaults to 0. Think of it as a labeled box that later modules can open to read the values they need, without hardcoding numbers into their own logic.

The record also comes with a property, ParamProps, that states both parameters are nonnegative. That is, any valid parameter record must have alpha ≥ 0 and Clag ≥ 0. This is a simple constraint, but it matters: it gives downstream code a guarantee that the numbers it receives are physically sensible, not negative artifacts.

In plain language, this establishes a convention: when other parts of the framework talk about relativity-related parameters, they agree to use this record and to respect the nonnegativity rule. It is a small piece, but it is the kind of foundation that lets larger proofs build without redefining their inputs each time.

/-- Minimal parameter record used by downstream modules. -/
structure Params where
  alpha : ℝ := 1
  Clag  : ℝ := 0

structure ParamProps (P : Params) : Prop :=
  (alpha_nonneg : 0 ≤ P.alpha)
  (Clag_nonneg : 0 ≤ P.Clag)

What this page does not claim

This module does not define the physical meaning of alpha or Clag. This module does not prove any theorem about relativity; it only defines a data structure and a property. This module does not establish the values of any physical constants.

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/Relativity/ILG/Params.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: