module module high

`IndisputableMonolith.Constants.KDisplay`

KDisplay module establishes the structural speed identity ℓ₀/τ₀ = c from Recognition Science units. Researchers auditing K-gate invariance or units consistency cite it when verifying dimensionless quotients under rescaling. The module organizes lemmas around the imported clock-side display period to derive the equality plus positivity and scale-invariance properties.

claimThe module establishes the identity ℓ₀/τ₀ = c, where ℓ₀ and τ₀ are the fundamental length and time yardsticks, together with display speed positivity and quotient invariance under admissible rescalings.

background

Recognition Science works in native units with c fixed to 1 while preserving structural relations between length and time scales. The upstream KDisplayCore supplies the clock-side display definition τ_rec(display) = (2π · τ₀) / (8 ln φ). This module translates that definition into the speed relation and checks invariance properties required for unit audits.

proof idea

This module organizes several short lemmas rather than a single proof. The central equality follows from substituting the display period into the speed expression and simplifying with the RS definition of c. Positivity and nonzero lemmas use direct evaluation; invariance follows from algebraic cancellation under rescaling.

why it matters in Recognition Science

It supplies the speed identity required by the downstream UnitsKGate certificate, which evaluates K-gate identities on canonical RS units packs and confirms the quotient remains dimensionless and invariant under admissible rescalings. The module therefore closes the structural link between display period and fundamental speed in the constants layer.

scope and limits

Does not derive the numerical value of c from deeper axioms.
Does not treat time-first versus length-first displays beyond the basic identity.
Does not connect to the phi-ladder mass formula or Berry threshold.
Does not include numerical checks against measured constants.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Certificates.UnitsKGate module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants.KDisplayCore module_import

declarations in this module (20)

lemma ell0_div_tau0_eq_c L16
lemma display_speed_eq_c_of_nonzero L24
lemma tau_rec_display_pos L35
lemma tau_rec_display_ne_zero L42
lemma display_speed_eq_c L45
theorem K_gate_units_invariant L53
theorem units_quotient_preserves_K L64
theorem single_inequality_audit L75
def K_gate_tolerance L81
def K_gate_check L89
theorem display_speed_positive L97
theorem display_ratio_scale_invariant L103
theorem display_rate_matches_structural_rate L114
theorem display_null_condition L131
def UnitsEquivalent L138
theorem displays_invariant_under_equivalence L168
structure KGateMeasurement L178
def validateKGate L193
def falsifier_K_gate_mismatch L198
theorem observable_factors_through_quotient L204