plan-strengthenedModelsImpDesign

Prompt file imported from petervdonovan/eagerdt-proofs (.github/prompts/plan-strengthenedModelsImpDesign.prompt.md). Copyright stays with the author.

Plan: Strengthened ModelsImp Design

Recommended direction: keep copyLeftToRight unchanged, keep bare containsDatatypes as the base notion, and introduce a new strengthened models_imp-style interface carrying the ANF-specific hypothesis only where that extra strength is needed.

Steps 0. Define Anf.hasIntendedInterpretation (struct : L.Anf.Structure M) : Prop that says: for every ground term t : L.GroundTerm, the ANF constant symbol .inr t : L.Anf.Functions 0 is interpreted as the realization of t (as an L-term) in the L-reduct of struct. Concretely:

∀ (t : L.GroundTerm),
  struct.funMap (.inr t) default =
    @FirstOrder.Language.Term.realize L M (Anf.anfModel2Model struct) Empty default t

Note: Anf.anfModel2Model struct is the L-reduct defined in R3_Flatten.lean using .inl functions only. This is what model2AnfModel preserves (it sets .inr t to t.realize), and hasIntendedInterpretation states that the converse holds for a general structure.

1. Define Anf.containsDatatypesAnf (ϕ : (QF_DT.Language G) →ᴸ L) (struct : L.Anf.Dup.Structure M) : Prop that bundles: (a) struct.containsDatatypes (ϕ.anf).dupL — the QF_DT embedding exists in the reduct (b) Anf.hasIntendedInterpretation for the left copy of the ANF constants: ∀ (t : L.GroundTerm), struct.funMap (.inl (.inr t : L.Anf.Functions 0)) default = @FirstOrder.Language.Term.realize L M struct_L Empty default t where struct_L : L.Structure M is the L-reduct obtained by composing the .inl (.inl ·) embedding (i.e., Anf.canonicalEmbedding.dupL reduct of struct). Condition (b) is what enables the key step in copied_model_rewriteSentence_constructor_iff: after copyLeftToRight, the right-copy constant .inr (.inr t) is mapped to .inl (.inr t) (by definition of copyLeftToRight), so if (b) holds for struct, then copyLeftToRight struct satisfies the same ANF constant equations for both copies.

2. Update models_imp in Dup.lean to use containsDatatypesAnf in place of bare containsDatatypes:

   def models_imp (Γ : L.Anf.Dup.Theory) (ϕ : (QF_DT.Language G) →ᴸ L) : Prop :=
     ∀ (M : Type w) (struct : L.Anf.Dup.Structure M),
       (Anf.containsDatatypesAnf ϕ struct ∧ struct ⊨ Γ) →
       copyLeftToRight struct ⊨ Γ
   

   The hypothesis containsDatatypes in the old definition is now replaced by the stronger containsDatatypesAnf. All call sites that construct a proof of models_imp will need to supply condition (b); all call sites that consume it will gain access to it.

   • R5_0_Embed.preserves_consistentLhs_imp_consistentRhs will need to verify (b) holds for the lift embedding (it should: lift_theory encodes exactly the ANF flattening equations that force the constant interpretations).
   • R5B_SelectorElim and R6_1_R6_2_TesterElim use models_imp only as an opaque hypothesis; their axiom stubs need their signatures updated but no new proof work.

3. Thread containsDatatypesAnf through the equisatisfiability chain as follows.

   Background: containsDatatypesAnf ϕ struct is strictly stronger than struct.containsDatatypes (ϕ.anf).dupL (it adds the ANF constant interpretation condition). Downgrading (forgetting condition b) is free; upgrading from bare containsDatatypes to containsDatatypesAnf requires a proof that condition (b) holds, which in general requires knowing that struct satisfies the ANF flattening equations (i.e. struct ⊨ Γ for some Γ that includes those equations). The lift_theory in R5_0_Embed is exactly such a theory.

   Axiom stubs (free to update, no proof to break):

   • R5B_SelectorElim.strongEquisatisfiability and equisatisfiability: replace struct.containsDatatypes (ϕ.anf).dupL with Anf.containsDatatypesAnf ϕ struct on both sides of the iff.
   • R6_1_6_2_TesterElim.strongEquisatisfiability and equisatisfiability: same replacement.
   • R6_2_2_Reduct.strongEquisatisfiabilityNoEmbedding: on the RHS, replace struct.containsDatatypes (ϕ.anf).dupL with Anf.containsDatatypesAnf ϕ struct.

   R5A_ConstructorElim.lean (real proof structure, handle carefully):

   • Change the existentials in strongEquisatisfiability and equisatisfiability from struct.containsDatatypes (ϕ.anf).dupL to Anf.containsDatatypesAnf ϕ struct.
   • Change copyLeftToRight_containsDatatypes conclusion from containsDatatypes to containsDatatypesAnf, and add a sorry for the new condition (b) component; the existing containsDatatypes subproof stays intact as the proof of (a).
   • In the proof body of strongEquisatisfiability, at each site that calls hconsistent' _ _ ⟨hleft, hsat⟩ where hleft : containsDatatypes ..., insert:

     have hAnf : Anf.containsDatatypesAnf ϕ struct := by
       sorry  -- TODO: derive from hleft + struct ⊨ Γ using ANF equations in Γ
     

     and pass hAnf instead of hleft.

   R5_0_Embed.lean (real proof, boundary theorem):

   • strongEquisatisfiability is the boundary between the L.Anf.Dup world and the L world. Its LHS currently states struct.containsDatatypes (lift_lhom ϕ) (i.e. struct.containsDatatypes (ϕ.anf).dupL). Change this to Anf.containsDatatypesAnf ϕ struct.
   • In the ← direction of the proof (lifting from L to L.Anf.Dup via expandAlong): after constructing the expanded struct, add a sorry for the new containsDatatypesAnf obligation. The existing containsDatatypes proof for (a) survives unchanged.
   • In the → direction (projecting from L.Anf.Dup to L): containsDatatypesAnf implies containsDatatypes, so the existing proof of the L-side containsDatatypes ϕ still works by projecting out component (a) of containsDatatypesAnf.

   Main.lean:

   • Replace struct.containsDatatypes ϕ' with Anf.containsDatatypesAnf ϕ struct in all intermediate have statements (reduct_noemb, tester_elim, selector_elim, constructor_elim, embed_equiv). The final goal and the initial rewrite ϕ Γ side are unchanged; only the intermediate Dup-world witnesses change predicate.

4. Annotate the unproved lemmas in Eagerdt/R5A_ConstructorElim.lean with brief comments stating how they should leverage the strengthened invariant, or questions if it seems like there is something wrong with how they are stated.

5. Add lemmas as needed to make the existing unproved lemmas easier to prove.

6. Fill in sorries in Eagerdt/R5A_ConstructorElim.lean, prioritizing work that is likely to uncover problems with the existing proof structure. Focus on copied_model_rewriteSentence_constructor_iff and preserves_consistentLhs_imp_consistentRhs

7. After the constructor slice is stabilized, revisit Eagerdt/Main.lean so that it compiles (with the existing sorries)

Relevant files

• /home/peter/school/219c/eagerdt/Eagerdt/Dup.lean — keep copyLeftToRight unchanged; add the strengthened models_imp-style abstraction here.
• /home/peter/school/219c/eagerdt/Eagerdt/R5A_ConstructorElim.lean — primary consumer of the stronger hypothesis; current proof gaps are here.
• /home/peter/school/219c/eagerdt/Eagerdt/Main.lean — top-level composition point that will need any interface split reflected cleanly.
• /home/peter/school/219c/eagerdt/Eagerdt/R5B_SelectorElim.lean
• /home/peter/school/219c/eagerdt/Eagerdt/R6_1_R6_2_TesterElim.lean
• /home/peter/school/219c/eagerdt/Eagerdt/R3_Flatten.lean — likely reference point for the meaning of ANF-generated constants when defining the stronger hypothesis.
• /home/peter/school/219c/eagerdt/Eagerdt/Basic.lean — supports the interpretation of dupL/dupR used in the copy semantics.

Verification

1. Files should type-check using Problems tool or lake build
2. Strengthened invariant should be used in place of current invariant
3. Summarize progress or roadblocks proving copied_model_rewriteSentence_constructor_iff and preserves_consistentLhs_imp_consistentRhs

Working Notes (added during steps 4–6)

Status of the sorries

• copyLeftToRight_containsDatatypes part (b): PROVED. The hard-coded L-reduct in containsDatatypesAnf only references .inl (.inl ·) symbols, and copyLeftToRight is the identity on .inl _. Both funMap (.inl (.inr t)) and the inline L-reduct used in (b) are unchanged when passing through copyLeftToRight; the proof is simpa from hleft.2 t.

• preserves_consistentLhs_imp_consistentRhs: BLOCKED on the same root cause as the constructor iff. The theorem hypothesis gives hsat : struct ⊨ rewrite ϕ Γ, NOT struct ⊨ Γ. Therefore hconsistent cannot be applied to struct directly — its precondition is struct' ⊨ Γ. The natural workaround would be to use copied_model_rewrite_iff.1 : copyLeftToRight struct ⊨ rewrite Γ ↔ copyLeftToRight struct ⊨ Γ to transport from rewrite to Γ, but that lemma's input side is the very goal of this theorem (circular). Furthermore, copied_model_rewrite_iff is itself derived from the BLOCKED copied_model_rewriteSentence_constructor_iff. So the two sorries here are genuinely blocked, not just unfilled. ONE of the two (hcopycopyΓ) becomes trivial if hcopyΓ is established (it then just applies hconsistent to copyLeftToRight struct using copyLeftToRight_containsDatatypes); we annotated this in code. NOTE: this also required adding an explicit universe annotation Dup.models_imp.{w} on both occurrences in the theorem signature; otherwise Lean infers two distinct universe variables and hconsistent cannot be applied to the local M.

Roadblock: copied_model_rewriteSentence_constructor_iff

The statement is, for a sentence equal const (.func (.inl (.inl f)) ts) whose RHS head function f : L.Functions l is a QF_DT-constructor (i.e. f = ϕ.onFunction (.inl f') for some f' : G.Functions l), modulo copyLeftToRight:

... ⊨ rewriteSentence ϕ (...) ↔ ... ⊨ .equal const (constructor application)

where rewriteSentence introduces tester(f', const), the constructor equation, and selectors.

• → direction: provable but tedious. Reduces to extracting the constructor clause from the rewritten conjunction and applying copyLeftToRight_models_dupR_eq to convert from dupR to dupL. (Type-elaboration noise around .inr f / .inl f coercions through L.Anf.Dup.Functions makes the proof fiddly but mechanical.) Currently subsumed under the single outer sorry for the whole iff.

• ← direction: BLOCKED. Must derive: (i) tester(f', const) and (ii) selectors_i(const) = ts i for each i, given only const = f(ts) (in the copy structure).

  The QF_DT.Structure G satisfies (i) and (ii) for every term of the form f(t1,...,tn), but containsDatatypes only states that QF_DT.Structure G embeds into the L-reduct; the embedding is not necessarily surjective. Concretely: we need to know that the value m := struct.funMap f (eval ts) lies in the image of the embedding. Without that, the embedding tells us nothing about RelMap (Tester f') m.

  containsDatatypesAnf (condition (b)) only constrains values of ANF constants .inl (.inr t) for ground t : L.GroundTerm. It says nothing about constructor applications to arbitrary terms ts. In particular, if const is not an ANF constant (which it generally is not in the constructor-elimination phase, because R5A operates on lift_theory Γ which has no ANF constants — see Main.lean and R5_0_Embed.lift_theory), then condition (b) does not apply.

  Conclusion: the ← direction of copied_model_rewriteSentence_constructor_iff is not provable from containsDatatypesAnf alone. To make it provable, one of the following must change:

  1. Strengthen the embedding hypothesis to a strict equality on the constructor fragment (e.g. reduct(struct, ϕ) = QF_DT.Structure G up to surjective embedding). Equivalently, restrict consideration to term-generated L-structures.
  2. Restrict the rewrite phase so that const is always a fresh ANF constant, and extend condition (b) to cover all constructor applications (not just constants). This effectively requires a prior ANF-flattening pass before R5A. The current R5_0_Embed.lift_theory does not flatten — see Main.lean for the order of transformations, which skips R3 entirely.
  3. Allow R5A to thread a syntactic side-condition (e.g. "every equation has the form equal anfConstant (constructorApp anfConstants)") and rely on (b) to compute the value of every subterm. This moves the term-model coverage from a semantic hypothesis to a syntactic invariant of the rewrite.

  Refinement after rereading the proof obligations: (2) and (3) are not really competing fixes in the current design. They operate at different levels:

  • (2) is the architectural / semantic repair. It changes the pipeline so that R5A is fed an ANF-shaped theory in the first place, with enough intended-interpretation coverage to compute constructor/selectors on the relevant terms.
  • (3) is the proof-level interface needed to use (2). Even if the pipeline is changed so R5A only ever receives ANF-shaped equations, the R5A lemmas are currently stated for arbitrary γ : L.Anf.Dup.Sentence. The proofs still need a threaded syntactic invariant saying that the specific γ under consideration has the ANF shape needed for condition (b) to apply.

  So the practical repair is probably: implement (2), then express its local consequence as (3). In other words, (2) supplies the missing truth of the statement; (3) supplies the missing hypothesis in the theorem statement/proof. Option (3) without (2) would only be enough if some earlier phase already guaranteed the ANF-shape invariant, which the current lift_theory pipeline does not.

Decision (going forward)

• Step 4 (annotation): DONE in-code.
• Step 5 (helper lemmas): no new lemmas needed yet; the existing @[simp] family of copyLeftToRight_* lemmas is sufficient for the parts that ARE provable.
• Step 6 (fill sorries): partially done.
  • copyLeftToRight_containsDatatypes part (b): proved.
  • preserves_consistentLhs_imp_consistentRhs: blocked (analysis above). One of two sorries reduces trivially given the other; both annotated in-code with the cycle.
  • copied_model_rewriteSentence_constructor_iff: blocked (analysis above). The subgoals are collapsed to a single outer sorry with detailed comment explaining the obstruction; previously they were 4 separate sorries with vague TODOs.
• Step 7 (Main.lean): no work required at this time. Main.lean already type-checks against the existing sorries, and no new sorry was introduced. Nothing to do until R5A is unblocked by a structural change to one of (1)/(2)/(3) above.

Verification

• lake build succeeds.
• R5A sorry count went from 4 to 3 (closed part (b) of copyLeftToRight_containsDatatypes).
• All other modules unchanged.

Recommended next step (out of scope for this turn)

Choose between (1)/(2)/(3) above. Option (2) is the most invasive but matches what the plan originally envisioned with Anf.hasIntendedInterpretation. Option (1) is the cleanest semantically but requires changing containsDatatypes itself, which would ripple across R5_0_Embed and beyond. Option (3) is the most conservative but requires proving (and threading) a new syntactic invariant on the output of lift_theory and each subsequent rewrite phase.

Update: after closer inspection, the likely viable path is not "choose exactly one" but "do (2), then expose the usable consequence as (3)". Option (1) remains a separate, stronger semantic alternative.

Next Steps

1. Introduce an explicit ANF-shape precondition for the constructor-elimination slice. The precondition should capture exactly the shape needed by condition (b): equations whose left side is an ANF constant and whose right side is either a constructor application to ANF constants or a sentence form preserved by the downstream rewrites. Do this at the sentence/theory level, not just informally in comments.

2. Rework the pipeline so R5A consumes ANF-shaped input rather than raw lift_theory Γ. Concretely, insert or expose the flattening information that guarantees the equations seen by R5A satisfy the predicate from step 1. This is the substantive implementation of (2). The current blocker is that R5_0_Embed.lift_theory preserves syntax but does not enforce ANF shape.

3. Thread the ANF-shape invariant through the R5A theorem statements. General lemmas like copied_model_rewriteSentence_constructor_iff are currently quantified over arbitrary γ : L.Anf.Dup.Sentence; that is too weak. Add the predicate from step 1 either as an explicit hypothesis or by restricting the theorem domain so the proofs can legally invoke containsDatatypesAnf condition (b).

4. Split copied_model_rewriteSentence_constructor_iff into two lemmas after step 3: one for the easy → projection direction, and one for the ← reconstruction direction under the new ANF-shape hypothesis. This will keep the proof obligations local and make it obvious which direction uses the stronger invariant.

5. Once the constructor iff is restated, revisit preserves_consistentLhs_imp_consistentRhs. At that point the circularity should disappear: copyLeftToRight struct ⊨ rewrite ϕ Γ can be converted to copyLeftToRight struct ⊨ Γ using the now-provable iff, and then the second application of hconsistent goes through with copyLeftToRight_containsDatatypes.

Progress on Next Steps (this turn)

Step 1 — DONE. Added in Eagerdt/R5A_ConstructorElim.lean:

• isAnfConst : L.Anf.Dup.Term (Empty ⊕ Fin 0) → Prop — "is .func (.inl (.inr c)) default for some c : L.GroundTerm".
• isAnfShapedSentence : L.Anf.Dup.Sentence → Prop — requires ANF constants on both sides of constructor-application equations; vacuously true on other sentence shapes (which rewriteSentence passes through).
• isAnfShapedTheory ϕ Γ : Prop — pointwise lift.

Step 3 — DONE. Threaded the predicate through R5A theorem statements:

• copied_model_rewriteSentence_iff now takes (hshape : isAnfShapedSentence γ).
• copied_model_rewrite_iff now takes (hshape : isAnfShapedTheory Γ).
• preserves_consistentLhs_imp_consistentRhs now takes the theory-level hypothesis.
• strongEquisatisfiability and equisatisfiability propagate it.
• Eagerdt/Main.lean updated: introduces have hshape_embed : ... := sorry (a single new sorry, marked with the formal step-2 obligation in a comment).

Step 4 — DONE. Split copied_model_rewriteSentence_constructor_iff into:

• copied_model_rewriteSentence_constructor_to (the easy →, no shape hypothesis needed).
• copied_model_rewriteSentence_constructor_from (the hard ←, takes hconst + hts).
• The original _iff is now a thin wrapper combining the two halves. Both _to and _from are currently sorry with detailed comments; the previous single sorry is now decomposed into two strictly-smaller obligations.

Step 5 — PARTIAL. preserves_consistentLhs_imp_consistentRhs was rewritten to use the new shape hypothesis. The previous double-sorry (with explicit cycle annotation) is now a single sorry (hcopyrew). The remaining obstruction is finer: even with the shape-strengthened iff, recovering struct ⊨ Γ from struct ⊨ rewrite ϕ Γ requires a models_rewrite_iff for an arbitrary struct (not just copyLeftToRight-image structures). This may decompose into another targeted lemma; recorded as a remaining obligation in-code.

Step 2 — DEFERRED. Pipeline integration (replacing/augmenting R5_0_Embed.lift_theory so it produces ANF-shaped theories, and likely restricting ground-term constants to the ϕ-image). This is the most invasive change and was scoped out for this turn. The hypothesis hshape_embed in Main.lean is the formal obligation that step 2 must discharge.

Step 6 — N/A. With step 2 deferred, no need to revisit Main's pipeline composition this turn.

Verification

• lake build succeeds.
• R5A sorry count: previously 3 (constructor_iff, hcopyΓ, plus old constructorElimination). Now 5 (constructorElimination, _to, _from, rewrite_preserves_anfShape, hcopyrew). The increase is by design: each new sorry is a smaller, more specific obligation than the lumped ones it replaced.
• Main.lean has 1 new sorry (hshape_embed) — the explicit pipeline-integration obligation (step 2).

Historical notes below are outdated

The notes in the next two sections are kept for history, but they predate two important corrections:

• the selector clauses in R5A.rewriteSentence now use dupL, not dupR;
• the missing hypothesis is no longer understood as a strengthened "G-fragment" version of isAnfConst, but as a theory-relative side-condition on admissible models.

As a result, any statements below about strengthening isAnfConst or needing a separate new obstruction for hcopyrew should be read as superseded.

Remaining hard work (outdated)

• (a) Strengthen isAnfConst to the G-fragment (require c = ϕ.onTerm c' for some G-ground term c'). This is what enables the ← (_from) direction to actually invoke containsDatatypes's embedding.
• (b) Discharge hshape_embed. Requires changing R5_0_Embed.lift_theory to produce ANF-flattened, G-fragment-restricted equations, possibly by composing with a variant of R3_Flatten.rewrite. This is the substantive content of step 2.
• (c) Discharge hcopyrew. Likely needs a new lemma models_rewrite_iff_arbitrary (i.e., the iff for arbitrary structures, not just copyLeftToRight images), or a different proof strategy that avoids it.

Update: more sorries closed (followup turn)

Filled in by direct proof:

• R5A.copied_model_rewriteSentence_constructor_to — the easy → direction. Proof: extract ϕ.onFunction (.inl f') = f from constructorPreimage? = some f' via Classical.choose_spec; then simp the Theory.Model of the rewritten union (which uses the @[simp] lemma copyLeftToRight_models_dupR_eq to convert dupR → dupL); apply the resulting universal to the constructor clause via Or.inl (Or.inr rfl); finally rewrite the dupL function symbol to .inl (.inl f) using the equation derived from hpre.
• R5A.rewrite_preserves_anfShape — by case-analysis on each clause produced by rewriteSentence. The pass-through cases trivially preserve shape; the constructor case produces only tester (rel — vacuously shaped), dupR-equal (head .inr ..., vacuously shaped), and selector equations (head .inr ..., vacuously shaped).

Added in R3_Flatten:

• Anf.isAnfConst, Anf.isAnfShapedSentence, Anf.isAnfShapedTheory — the L.Anf-level analogs of the L.Anf.Dup-level predicates in R5A. (At the L.Anf level the constructor head is .inl _, vs .inl (.inl _) after lifting.)
• Anf.isAnfConst_fromGroundTerm_asConst — helper showing fromGroundTerm (asConst t) is canonically ANF-constant.
• Anf.flatten_term_isAnfShaped — by induction on the ground term, with flatten_term's inductive structure folded out by simp.
• Anf.flatten_sentence_head_isAnfShaped — case-analysis on sentence shape; equality cases produce ANF-constants on both sides, so the constructor pattern of isAnfShapedSentence (which requires a .inl _ head on the RHS) does not fire.
• Anf.rewrite_sentence_isAnfShaped and Anf.rewrite_isAnfShaped — these glue together via membership unfolding.

Remaining R5A sorries (outdated wording)

• constructorElimination (line ~125) — preexisting, unrelated.
• copied_model_rewriteSentence_constructor_from — the hard ← direction.
• hcopyrew inside preserves_consistentLhs_imp_consistentRhs — same structural blocker as _from.

The diagnosis in these bullets is outdated: after the selector change to dupL, the remaining local obstruction is better phrased as a theory-relative side-condition on models saying that the relevant ANF constants denote elements in the embedding image. hcopyrew no longer appears to need a separate idea beyond whatever is needed to prove _from under that side-condition.

Bridge work still owed (outdated ordering)

• Bridge lemma in R5A: Anf.isAnfShapedTheory Γ → R5A.isAnfShapedTheory ϕ ((LHom.id L.Anf).dupL.onTheory Γ). The L.Anf-level shape lifts cleanly through dupL because dupL.onTerm only adds .inl wrappers without touching the function-symbol structure that isAnfShapedSentence inspects.
• Pipeline change in Eagerdt/Main.lean: insert R3 flattening between R5_0_Embed.lift_theory (or a refactored variant) and R5_A_ConstructorElim.rewrite. This will discharge hshape_embed (the only sorry in Main.lean).

Update: what we learned after revisiting the obstruction

• The earlier phrase "the ANF constants' underlying ground terms must lie in the ϕ-image" was too strong and not quite the right invariant. It would push too much syntax into the QF_DT fragment and would conflict with the role of uninterpreted constants in satisfiability.
• The real gap is semantic, not purely syntactic. containsDatatypes only constrains the reduct on tuples already lying in the image of the embedding QF_DT.Structure G ↪ reduct(struct, ϕ). The blocked R5A proofs need to know that the specific values touched by constructor equations are in that image.
• Condition (b) of containsDatatypesAnf is still useful, but only for identifying the denotations of ANF constants with realizations of L-ground terms. By itself it does not imply that those denotations lie in the embedding image.
• So the missing hypothesis is better understood as a well-formedness / image-closure side-condition on the models we care about: for the relevant ANF constants occurring in the theory slice under consideration, their interpretations land in the image of the chosen embedding. Once that holds, constructor applications on those values also stay in the image by homomorphism preservation, and the tester/selector clauses can be derived inside the embedded QF_DT fragment.
• This new condition is theory-relative. It should probably not be folded directly into containsDatatypesAnf, which is currently a pure model-side predicate. Instead it should be threaded separately through the R5A lemmas that actually need it, as a side-condition refining which models of the theory are admissible for the constructor-elimination argument.

Current completion plan for R5A_ConstructorElim

These are the steps that now seem specifically necessary to complete Eagerdt/R5A_ConstructorElim.lean, as opposed to later integrating it back into Main.lean.

1. Define a theory- or sentence-relative side-condition on models expressing image membership for the relevant ANF constants. The minimal useful form is: given a witness embedding for containsDatatypes, every ANF constant appearing in the sentence/theory slice under analysis denotes an element in the range of that embedding.

2. Thread that side-condition through the local R5A lemmas that actually need it. At minimum, copied_model_rewriteSentence_constructor_from should take it explicitly. preserves_consistentLhs_imp_consistentRhs should then depend on the same side-condition only through that local reconstruction lemma, not through a separate new hypothesis about right-copy symbols.

3. Prove copied_model_rewriteSentence_constructor_from under that side-condition. This is now the main semantic proof obligation: use condition (b) of containsDatatypesAnf to identify the ANF-constant denotations, use the side-condition to place those denotations in the embedding image, and then use the QF_DT constructor/tester/selector semantics in the embedded fragment to derive the rewritten clauses.

4. Reuse that local proof to finish preserves_consistentLhs_imp_consistentRhs. After switching selector clauses to dupL, hcopyrew no longer appears to require a separate counterexample-avoiding argument. It should collapse once _from is available under the right side-condition.

5. Prove constructorElimination as the remaining separate structural theorem about the syntax of rewrite. This theorem is orthogonal to the semantic side-condition work above.

Later integration work

The following items are likely still needed for the full pipeline, but they are not part of the minimal set of steps required to complete R5A_ConstructorElim itself.

1. Add the ANF-shape bridge from R3_Flatten into the R5A input. This is the existing bridge lemma about lifting Anf.isAnfShapedTheory through dupL.

2. Add the bridge from the flattening output to the new theory-relative side-condition. This should be phrased carefully: flattening outputs a theory, not a structure, so it should characterize an admissible class of models rather than directly define denotations.

3. Revisit Main.rewrite once both bridges exist. At that point the pipeline should thread both:

• an ANF-shape bridge from R3 into R5A, and
• the new side-condition on admissible models needed by the remaining R5A semantic lemmas.

Progress update on later integration work

• Step 1 is now implemented in Eagerdt/R5A_ConstructorElim.lean via:

  • dupL_preserves_isAnfConst
  • dupL_preserves_isAnfShapedSentence
  • dupL_preserves_isAnfShapedTheory

• Step 2 is blocked under the current global definition of Dup.anfConstsInImage / Dup.containsDatatypesAnfWellSorted. The issue is semantic, not proof-search noise: R3_Flatten.rewrite introduces ANF constants for arbitrary L.GroundTerms coming from subterms of Γ, while the containsDatatypes ϕ embedding only controls the QF_DT fragment. There is no reason, in general, that every ANF constant produced by flattening should denote an element in the image of that embedding.

• Consequence: Main cannot yet replace the old unflattened R5A input with a flattened one and still discharge the stronger R5A/R5A-adjacent witness obligations by a generic bridge from struct.containsDatatypes ϕ.

• To resume integration cleanly, one of these design changes is needed:

  1. Relax anfConstsInImage back to a theory-relative/image-on-relevant-constants condition.
  2. Restrict the flattened constants to a syntactically identified ϕ-image fragment.
  3. Strengthen the semantic boundary theorem so it assumes/proves a genuinely global image closure property, which is stronger than the current containsDatatypes ϕ interface.

Plan for threading a non-Anf well-sortedness condition through the pipeline

If Main.equisatisfiability should stay free of Anf-specific predicates, the cleanest way to thread the stronger invariant is to move the image-closure statement to the L boundary and then prove that R5_0_Embed preserves/reflects it.

Proposed boundary predicate on L.Structure

Define an L-side well-sortedness predicate that does not mention ANF constants:

def FirstOrder.Language.Structure.groundTermsInEmbeddingImage
  (ϕ : (QF_DT.Language G) →ᴸ L) (struct : L.Structure M) : Prop :=
  ∃ e : (QF_DT.Structure G) ↪[QF_DT.Language G] @FirstOrder.Language.LHom.reduct _ L ϕ M struct,
    ∀ t : L.GroundTerm, ∃ g : G.GroundTerm, e g = struct.realize default t

This is the L-structure analogue of the current global Dup.anfConstsInImage:

• on the Dup side, left-copy ANF constants denote realizations of L.GroundTerms;
• on the L side, the same information is stated directly as image-membership of ground-term realizations.

The key advantage is that Main.equisatisfiability can mention this predicate without mentioning Anf or L.Anf.Dup in its statement.

Refactor steps

1. Add the new L-side predicate in a boundary-appropriate file. Most likely Eagerdt/QF_DT.lean, Eagerdt/Reduct.lean, or Eagerdt/R5_0_Embed.lean. It should live near containsDatatypes, since it is a strengthening of the same semantic embedding interface.

2. Prove the two conversion lemmas in R5_0_Embed.lean.

• Dup.containsDatatypesAnfWellSorted ϕ struct_dup -> groundTermsInEmbeddingImage ϕ (lhom.reduct M)
• struct.containsDatatypes ϕ -> groundTermsInEmbeddingImage ϕ struct -> Dup.containsDatatypesAnfWellSorted ϕ struct_dup

The first direction should use:

• component (a) of containsDatatypesAnfWellSorted for the embedding witness;
• component (b) of containsDatatypesAnf to identify left-copy ANF constants with L.GroundTerm realizations;
• anfConstsInImage to place those left-copy ANF constant values in the embedding image.

The second direction should use the existing struct_dup construction from R5_0_Embed.strongEquisatisfiability:

• component (a) of Dup.containsDatatypesAnfWellSorted comes from the existing containsDatatypes proof;
• component (b) is already proved via Anf.model2AnfModel;
• the new anfConstsInImage component should follow from the L-side well-sortedness hypothesis because ANF constants in struct_dup realize exactly the underlying ground terms in struct.

3. Update R5_0_Embed.strongEquisatisfiability and equisatisfiability. Replace the current RHS struct.containsDatatypes ϕ ∧ struct ⊨ Γ with struct.containsDatatypes ϕ ∧ groundTermsInEmbeddingImage ϕ struct ∧ struct ⊨ Γ.

On the LHS, replace Dup.containsDatatypesAnf with Dup.containsDatatypesAnfWellSorted.

4. Thread the stronger duplicated-language witness through the post-R5A pipeline. Update the intermediate existentials in:

• R5B_SelectorElim
• R6_1_R6_2_TesterElim
• R6_2_2_Reduct
• Main

so that the duplicated-language side carries Dup.containsDatatypesAnfWellSorted ϕ struct instead of only Dup.containsDatatypesAnf ϕ struct.

These files mostly use the predicate opaquely, so this should be interface work rather than new semantic proof work.

5. Update Main.equisatisfiability to use the stronger L-side boundary condition. Its RHS should become:

∃ struct : L.Structure M,
  struct.containsDatatypes ϕ ∧
  groundTermsInEmbeddingImage ϕ struct ∧
  struct ⊨ Γ

This keeps Main free of Anf, while making explicit the exact global well-sortedness assumption needed to justify the stronger duplicated-language witnesses.

6. Only after that, revisit whether Dup.anfConstsInImage should stay global. If the global version becomes too strong for the eventual flattening-based pipeline, we can still relax it later to a theory-relative condition. But the threading work above cleanly exposes whether the current global notion is actually what the end-to-end theorem wants.

Expected outcome of this plan

• Main states the stronger semantic contract in L-language terms.
• R5_0_Embed becomes the only file responsible for translating that contract into the duplicated-language invariant.
• The post-R5A stages carry a single strengthened duplicated-language witness shape.
• If a remaining obstruction persists, it will be localized to whether the global image condition is the right boundary theorem, rather than hidden inside Main's chaining proof.