LogicRealization
Why this theorem is linked from Homomorphic Directional Beamforming with Analog True Time Delay Arrays echoes
Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.
Corollary 1. ∀Φ1, Φ2 ∈ V1, PΦ1+Φ2 = PΦ1 ⋆ PΦ2; <PT, ⋆> defines a group structure
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.
plain-language theorem explainer
LogicRealization assembles the minimal interface any Law-of-Logic realization must supply to feed arithmetic extraction in the Universal Forcing program. Researchers mapping continuous ratios, discrete propositions, or categorical settings into arithmetic cite this structure to guarantee an orbit isomorphic to LogicNat together with identity-step data. The declaration is the structure definition that packages carrier, cost, step, interpretation, and the three open propositions without further derivation.
Claim. A structure consisting of a carrier set $C$, cost type $K$ with zero, comparison map $C×C→K$, zero element and step map on $C$, an orbit type $O$ with its own zero and step, an interpretation $O→C$ preserving zero and step, an equivalence $O≃LogicNat$ preserving zero and successor, the axioms that compare is reflexive and symmetric, plus three propositions (excluded middle, composition, action invariance) and the existence of a nontrivial element in $C$.
background
The module creates a setting-independent interface for the Universal Forcing program so that distinct Law-of-Logic settings can be mapped to a common object. LogicNat is the inductive type with constructors identity and step that mirrors the smallest subset of positive reals closed under multiplication by the generator and containing 1. ArithmeticOf R is the structure that extracts a Peano object and its initiality from any such realization R.
proof idea
This declaration is the structure definition that collects the required fields and propositions; no separate proof body exists.
why it matters
LogicRealization is the parent structure for ArithmeticOf and its derived objects canonical, extracted, and their PeanoSurface theorems. It supplies the identity-step orbit data from which initial Peano objects are lifted and equivalences between realizations are constructed. The module doc states that the invariant target is the arithmetic object extracted from the identity-step data, placing the structure at the entry point of the forcing chain before T5 J-uniqueness and T6 phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
TTD homomorphism yields low-memory split-beam dictionary
"Corollary 1. ∀Φ1, Φ2 ∈ V1, PΦ1+Φ2 = PΦ1 ⋆ PΦ2; <PT, ⋆> defines a group structure"