module module high

`IndisputableMonolith.Foundation.StillnessGenerative`

The StillnessGenerative module defines non-trivial configurations as those differing from the uniform ground state of all entries equal to 1. It supplies the phi-ladder sequence and related predicates such as is_nontrivial to mark departures from trivial stillness. Researchers working on the transition from low-entropy initial conditions to structured states cite these definitions when applying self-similarity arguments. The module consists entirely of definitions and basic lemmas with no central theorem proof.

claimA configuration $c$ is non-trivial if there exists an index $i$ such that $c_i = 1$ fails, equivalently if $c$ is not the uniform ground state.

background

This module operates in the Foundation layer, importing the Law of Existence (x exists iff defect(x) = 0), PhiForcing (phi forced by self-similarity in a discrete ledger with J-cost), PhiForcingDerived (r² = r + 1 from discrete scale and additive ledger axioms), InitialCondition (formalizing the low-entropy start), and Cost. It introduces the phi-ladder as the geometric sequence of self-similar scales together with the predicate is_nontrivial that distinguishes structured states from the all-ones trivial configuration.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The non-triviality and phi-ladder definitions feed the sibling results T4_Recognition, has_phi_structure, and phi_ladder_positive_cost inside the same module. They supply the criterion for moving from the uniform ground state to generative structure, closing the step between the phi-forcing axioms and the recognition of non-trivial states required for the forcing chain.

scope and limits

Does not prove any theorem about physical constants or dimensions.
Does not derive the value of phi or the eight-tick octave.
Does not address dynamics, time evolution, or measurement.
Does not contain the full forcing chain from T0 to T8.

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.InitialCondition module_import
IndisputableMonolith.Foundation.LawOfExistence module_import
IndisputableMonolith.Foundation.PhiForcing module_import
IndisputableMonolith.Foundation.PhiForcingDerived module_import

declarations in this module (39)

def phi_ladder L44
theorem phi_ladder_pos L46
theorem phi_zpow_ne_one L49
theorem phi_ladder_ne_one L57
theorem phi_ladder_positive_cost L62
theorem phi_cost_eq L66
theorem phi_cost_pos L69
theorem phi_perturbation_bounded L72
def has_phi_structure L77
theorem unity_has_no_phi_structure L80
def is_nontrivial L105
structure T4_Recognition L120
theorem nontrivial_closed_has_phi_structure L136
theorem t6_derived L161
theorem ground_state_recognition_impossible L177
theorem static_ground_state_impossible L186
def eight_tick_period L212
def cycle_nondegenerate L217
theorem uniform_cycle_degenerate L221
theorem eight_tick_forces_nontrivial L235
theorem eight_tick_breaks_uniformity L244
theorem perturbation_cost_quadratic L250
theorem perturbation_cost_positive L254
theorem perturbation_cost_small_bound L258
theorem dalembert_cascade L264
theorem phi_power_compose L271
theorem phi_power_ratio L275
theorem ladder_cascade_bound L279
theorem doubling_cascade L287
theorem doubling_cascade_positive L300
theorem fibonacci_cascade L320
theorem one_plus_phi_eq_phi_sq L332
theorem closure_populates_next L341
theorem every_rung_from_fibonacci L353
theorem ledger_symmetry_negative_rungs L363
theorem stillness_is_creative L397
theorem ground_state_paradox L431
theorem origin_question_resolved L443
theorem symmetry_breaking_mechanism L463