mastery_one_statement
plain-language theorem explainer
The theorem states that the baseline per-rung mastery cost is exactly 45 hours, that each additional rung multiplies total cost by phi, and that costs rise strictly with rung index. Researchers modeling skill acquisition from the consciousness gap would cite it to recover Ericsson's 10,000-hour rule as a phi^7 jump from the 45-hour floor. The proof is a one-line term that directly packages the three already-proved component facts.
Claim. The per-rung cost equals 45, the mastery cost satisfies $c(N+1)=c(N)·ϕ$ for every natural number $N$, and $c(N)<c(M)$ whenever $N<M$.
background
The module derives Ericsson's expert-performance rule from the Recognition Science phi-ladder. Per-rung cost is defined as the constant 45 (equal to consciousnessGap 3 applied to skill acquisition). Mastery cost at rung $N$ is then $45·ϕ^N$. The three supporting facts are: perRungCost_eq (the constant equals 45), masteryCost_succ (cost multiplies by phi on each rung advance), and masteryCost_strict_mono (costs increase strictly with rung index, proved via positivity of 45 and the fact that $1<ϕ$).
proof idea
The proof is a term-mode construction that directly returns the triple of the three component results: perRungCost_eq for the constant, masteryCost_succ for the multiplicative step, and masteryCost_strict_mono for the ordering. No additional tactics are applied.
why it matters
This packages the core quantitative claims of the Mastery Threshold from Gap-45 track. It supplies the explicit cost formula used to bracket the 10,000-hour rule as the phi^7 jump from the 45-hour baseline and the full ladder to rung 17 as approximately 88,000 hours. The result sits inside the Recognition Science derivation of human performance limits from the phi fixed point and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.