extracted
The extracted definition assembles the arithmetic object for any Law-of-Logic realization by taking its Peano component directly from the realization orbit and confirming initiality via the pre-established witness. Researchers deriving arithmetic from abstract logic structures cite this when applying universal forcing. The construction is a direct record assembly delegating to realizationPeano and realization_initial.
claimFor a Law-of-Logic realization $R$, the extracted arithmetic is the structure whose Peano object is the orbit of $R$ under its zero and step operations, equipped with the initiality property that every other Peano object admits a unique homomorphism from it.
background
A Law-of-Logic realization consists of a carrier set, a comparison cost, an identity element, and a generator step together with the structural propositions that allow arithmetic extraction. The ArithmeticOf structure packages a Peano object with a proof that the object is initial among all Peano objects. The upstream realizationPeano constructs the Peano object from the realization's orbit, zero, and step fields, while realization_initial supplies the unique-lift property.
proof idea
The definition is a one-line wrapper that applies realizationPeano to obtain the Peano object and realization_initial to obtain the initiality witness, then assembles the two fields into the ArithmeticOf record.
why it matters in Recognition Science
This definition supplies the canonical arithmetic object extracted from any realization and is invoked by extracted_peanoSurface to establish Peano surface properties and by realization_initial to confirm initiality. It realizes the step in the forcing chain where identity-step data generate the initial Peano algebra, the mechanism behind Universal Forcing. The construction closes the loop from abstract realizations to concrete arithmetic without additional hypotheses.
scope and limits
- Does not specify a concrete carrier set or numerical values inside the realization.
- Does not prove existence of realizations beyond the supplied structure fields.
- Does not address physical constants or the phi-ladder.
- Does not extend to non-initial Peano objects or non-forced arithmetic.
Lean usage
def test (R : LogicRealization) : ArithmeticOf R := extracted Rformal statement (Lean)
197def extracted (R : LogicRealization) : ArithmeticOf R where
198 peano := realizationPeano R
proof body
Definition body.
199 initial := realization_initial R
200
201/-- Peano surface for the extracted arithmetic of any realization. -/
used by (33)
-
aggCoeff_flatMap -
toMoves -
extracted_peanoSurface -
logicNat_initial -
realizationFold -
realization_initial -
realizationLift_unique_fun -
ContinuityFromFiniteDescription -
RegularityCert -
StrictConvexityFromClosure -
GaugeLayer -
continuous_combiner_log_smoothness_bootstrap -
SatisfiesLawsOfLogicContinuous -
excluded_middle_implies_continuous -
modularRealization -
physics_faithful -
arithmeticOf -
toLightweight -
tendsto_exp_neg_mul_ofReal_atTop -
gap1_absorptive_not_stable -
Status -
rm2Closed_of_bet2 -
WitnessedDefectSensor -
phaseIncrementEpsilonBound_decreasing -
electron_structural_ratio -
page_entropy_max_at_half -
UnitsEqv -
YukawaNormalizationHypothesis -
yukawa_SM_phi_pow_scaling -
annularCost_nonneg