RGConditionsForDualityHypothesis
plain-language theorem explainer
This hypothesis interface stands in for the RG Conditions for Duality proposition appearing in DraftV1.tex. Authors formalizing duality derivations within quotient topologies would cite it while the supporting topology remains open. The declaration reduces to the constant true proposition, providing a temporary scaffold rather than a derived result.
Claim. The conditions required for duality in the recognition geometry hold as an assumption.
background
The Papers.DraftV1 module mirrors theorem statements from Draft_v1.tex. Where full formalization is unavailable, such as propositions depending on the topology of quotients and local contractibility, the module supplies explicit hypothesis interfaces instead of global axioms. This keeps any downstream theorems conditional on the supplied hypotheses. No upstream lemmas are referenced.
proof idea
The declaration is a one-line definition that sets the hypothesis to the proposition True.
why it matters
The hypothesis is consumed by the theorem rg_conditions_for_duality, which returns a trivial conclusion and serves as placeholder for the paper proposition on RG Derivation of Central Potentials. It marks an open formalization gap for duality in quotient spaces. The status note in the module doc-comment identifies the missing pieces as topology of quotients plus local contractibility.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.