module module moderate

`IndisputableMonolith.Linguistics.LexiconRatio`

The LexiconRatio module supplies the Recognition Science prediction for the active-vocabulary fraction in language. It assembles phi_inv, passive_fraction, and the sum-to-one relation to isolate the active complement. Quantitative linguists and RS modelers cite it when mapping the phi-ladder onto lexical statistics. The module is built from definitions and elementary lemmas imported from Constants and Cost.

claimThe predicted active-vocabulary fraction equals $1 - p$, where the passive fraction $p = phi^{-2}$ and the two fractions sum to one.

background

Recognition Science obtains phi as the unique self-similar fixed point of the J-cost map (T6). The module imports the RS time quantum tau_0 = 1 tick from Constants and the cost structures from Cost. It defines phi_inv as the inverse golden ratio, passive_fraction as its square inverse, and proves the two fractions are complementary and positive.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the active-vocabulary fraction that extends the phi-ladder and eight-tick octave into linguistics. It fills the step that converts the J-uniqueness and RCL identities into a concrete lexical observable. No downstream theorems are yet recorded.

scope and limits

Does not derive the fraction from empirical corpora.
Does not model language-specific deviations.
Does not address syntax or semantics.
Does not incorporate time evolution of the lexicon.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (20)

def phi_inv L70
theorem phi_inv_pos L72
theorem phi_inv_lt_one L75
theorem phi_inv_band L80
theorem phi_sq L92
theorem phi_inv_fibonacci_fixed_point L98
theorem fib_fn_strict_mono L114
theorem phi_inv_unique L122
def passive_fraction L139
theorem passive_fraction_pos L141
theorem passive_fraction_eq_phi_sq_inv L145
theorem fractions_sum_to_one L152
def lexicon_ratio L160
theorem lexicon_ratio_pos L162
theorem lexicon_ratio_lt_one L163
theorem lexicon_ratio_band L165
theorem lexicon_ratio_derivation L170
structure LexiconRatioCert L186
def lexiconRatioCert L194
theorem lexicon_ratio_one_statement L214