pith. sign in
module module high

IndisputableMonolith.Cosmology.ScaleInvarianceSelectionCert

show as:
view Lean formalization →

The ScaleInvarianceSelectionCert module certifies scale invariance in cosmology by formalizing the Recognition Composition Law as a cost-control relation. Researchers deriving cosmological models from the J-cost and phi-ladder would cite it to justify why scale transformations incur no extra cost. The module assembles its argument from lemmas on equality cases, scale-change costs, and log-space symmetry.

claimThe central object is the scale invariance certificate asserting that when the J-cost satisfies $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$, scale transformations leave the total cost unchanged on the phi-ladder.

background

The module sits in the cosmology domain and imports the J-cost definition together with the base time quantum τ₀ = 1 tick. It relies on the Recognition Composition Law (RCL) whose doc-comment states: 'The Recognition Composition Law (RCL) in inequality form: J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The cost of combining x and y is controlled by their individual costs.' Sibling declarations introduce scale_change_cost, no_scale_change_is_free, and log_space_symmetry to support the certificate.

proof idea

The module organizes its argument as a chain of supporting lemmas: rcl_equality, scale_change_cost, no_scale_change_is_free, and log_space_symmetry. These establish cost preservation under scaling before the final ScaleInvarianceCert is stated. It functions as a certificate module that composes results from the Cost and Constants imports.

why it matters in Recognition Science

The module supplies the ScaleInvarianceCert that feeds scale selection into broader cosmological derivations. It fills the step that selects scale-invariant models consistent with the eight-tick octave and D = 3. No used_by relations are recorded, indicating it serves as a foundational certificate rather than a terminal result.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)