min_max_achieved
The declaration establishes that the positive integer pair (1,1) attains the value 1 under the max function. Researchers closing the zero-parameter ledger to hierarchical structure in Recognition Science cite it to anchor the base rung before invoking uniform scaling. The term-mode proof reduces the equality by direct simplification of the max expression.
claimFor positive integers $a$ and $b$, the pair $(1,1)$ satisfies $a=1$, $b=1$ and therefore achieves the minimal value of the maximum function equal to 1.
background
The module closes Gap 2 of the axiom-closure plan by deriving hierarchical structure from the nontrivial zero-parameter ledger. It defines ScalePerturbed as an explicit perturbation shifting levels above a chosen position by exp(t) and proves that uniform inter-level ratios are forced once the zero-parameter condition holds. The sibling result additive_composition_is_minimal states that among positive-integer pairs the pair (1,1) uniquely minimises max(a,b) by pure arithmetic.
proof idea
One-line wrapper that applies simp to reduce the max expression directly to the constant 1.
why it matters in Recognition Science
The result supplies the arithmetic base case for the minimal-coefficients claim inside the hierarchy-forcing sequence. It precedes the derivation of uniform_scaling_forced and hierarchy_forced_gives_phi, which together force the self-similar phi-ladder from the Recognition Composition Law. No open scaffolding remains at this leaf.
scope and limits
- Does not prove uniqueness of the minimizing pair without the sibling additive_composition_is_minimal.
- Does not extend the minimality claim beyond positive integers.
- Does not invoke the Recognition Composition Law or any forcing-chain step T5-T8.
- Does not address perturbations or non-uniform ratios.
formal statement (Lean)
116theorem min_max_achieved : max 1 1 = 1 := by simp
proof body
Term-mode proof.
117
118/-- Any other pair has max ≥ 2. -/